module My.README where

-- §──────────────────────────────────────────────────────────────────
-- These are my efforts with Agda.  Often they are just helper
-- functions which seemed worth abstracting out.
-- §──────────────────────────────────────────────────────────────────


-- §──────────────────────────────────────────────────────────────────
-- Set theory.
-- §──────────────────────────────────────────────────────────────────

open import My.SetTheory.Fin
open import My.SetTheory.Induction
open import My.SetTheory.Nat
open import My.SetTheory.Relation
open import My.SetTheory.Sum

-- §──────────────────────────────────────────────────────────────────
-- Algebra
-- §──────────────────────────────────────────────────────────────────

open import My.Algebra.Structure

-- §──────────────────────────────────────────────────────────────────
-- Miscellany
-- §──────────────────────────────────────────────────────────────────

-- §──────────────────────────────────────────────────────────────────
-- Surds in cancellative commutative monoids, following Thierry
-- Coquand (http://www.cs.ru.nl/~freek/comparison/files/agda.alfa), and
-- Ikegami Daisuke (https://github.com/IKEGAMIDaisuke/Pythagoras)
-- §──────────────────────────────────────────────────────────────────

--   Let A be a cancellative commutative semigroup, and π an element
--   of A.  Define a relation _⊰_ on A by
--
--     x ⊰ y = π ∙ x ≈ y,
--
--   where _∙_ is the binary operation on A, and _≈_ is the equality
--   on A.  Suppose that the relation _⊰_ does not have infinite
--   descent.  Then, π is a surd, that is,
--
--     (x y : A) → ¬ a ∙ square x ≈ square y

open import My.Surd.CancellativeCommutativeMonoid