shifting to main branch as suggested by Wen

src/Equivalence.lagda

@@ -0,0 +1,47 @@
+---
+title     : "Equivalence: Martin Löf equivalence"
+layout    : page
+permalink : /Logic
+---
+
+## Equivalence
+
+Much of our reasoning has involved equivalence.  Given two terms `M`
+and `N`, both of type `A`, we write `M ≡ N` to assert that `M` and `N`
+are interchangeable.  So far we have taken equivalence as a primitive,
+but in fact it can be defined using the machinery of inductive
+datatypes.
+
+We declare equivalence as follows.
+\begin{code}
+data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
+  refl : x ≡ x
+\end{code}
+In other words, for any type `A` and for any `x` of type `A`, the
+constructor `refl` provides evidence that `x ≡ x`.  Hence, every
+value is equivalent to itself, and we have no way of showing values
+are equivalent.  Here we have quantified over all levels, so that
+we can apply equivalence to types belonging to any level.
+
+We declare the precedence of equivalence as follows.
+\begin{code}
+infix 4 _≡_
+\end{code}
+We set the precedence of `_≡_` at level 4, the same as `_≤_`,
+which means it binds less tightly than any arithmetic operator.
+
+[CONTINUE FROM HERE. FIND A SIMPLE PROOF USING REWRITE.]
+
+Including the lines
+\begin{code}
+{-# BUILTIN EQUALITY _≡_ #-}
+{-# BUILTIN REFL refl #-}
+\end{code}
+permits the use of equivalences in rewrites.  When we give
+a proof such as 
+
+\begin{code}
+cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
+cong f refl = refl
+\end{code}
+

src/Logic.lagda

@@ -1,28 +1,11 @@
 ---
-title     : "Logic: Propositions as Type"
+title     : "Logic: Propositions as Types"
 layout    : page
 permalink : /Logic
 ---
 
-This chapter describes the connection between logical connectives
-(conjunction, disjunction, implication, for all, there exists,
-equivalence) and datatypes (product, sum, function, dependent
-function, dependent product, Martin Löf equivalence).
-
-## Imports
-
-\begin{code}
-import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_; refl; sym; trans; cong; cong-app)
-open Eq.≡-Reasoning
-open import Data.Nat using (ℕ; zero; suc)
-open import Agda.Primitive using (Level; lzero; lsuc)
-\end{code}
-
-This chapter introduces the basic concepts of logic, including
-conjunction, disjunction, true, false, implication, negation,
-universal quantification, and existential quantification.
-Each concept of logic is represented by a corresponding standard
+This chapter introduces the basic concepts of logic, by observing
+that each concept of logic is represented by a corresponding
 data type.
 
 + *conjunction* is *product*
@@ -34,9 +17,19 @@ data type.
 + *universal quantification* is *dependent function*
 + *existential quantification* is *dependent product*
 
-We also discuss how equality is represented, and the relation
-between *intuitionistic* and *classical* logic.
+We also discuss the relation between *intuitionistic* and *classical*
+logic.
 
+## Imports
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Properties.Simple using (+-suc)
+open import Agda.Primitive using (Level; lzero; lsuc)
+\end{code}
 
 ## Isomorphism
 
@@ -808,7 +801,7 @@ to the left and application associates to the right.  Thus
 
 and
 
-   f x y    *stands for*   (f x) y
+    f x y    *stands for*   (f x) y
 
 Currying is named for Haskell Curry, after whom the programming language Haskell
 is also named.  However, Currying was introduced earlier by both Gotlob Frege
@@ -1150,8 +1143,8 @@ to introduce `x` as a bound variable.
 We formalise existential quantification by declaring a suitable
 inductive type.
 \begin{code}
-data ∃ : ∀ {A : Set} → (A → Set) → Set where
-  _,_ : ∀ {A : Set} {B : A → Set} → (x : A) → B x → ∃ B
+data ∃ {A : Set} (B : A → Set) : Set where
+  _,_ : (x : A) → B x → ∃ B
 \end{code}
 Evidence that `∃ (λ (x : A) → B[x])` holds is of the form
 `(M , N)` where `M` is a term of type `A`, and `N` is evidence
@@ -1171,11 +1164,96 @@ instantiate that proof that `∀ (x : A) → B[x] → C` to any `x`, and we
 may choose the particular `x` provided by the evidence that `∃ (λ (x :
 A) → B[x])`.
 
-The types `¬ (∃ (λ (x : A) → B[x]))` and `∀ (x : A) → ¬ B[x]` are isomorphic.
-\begin{code}
-extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
-extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
 
+[It would be better to have even and odd as an exercise.  Is there
+a simpler example that I could start with?]
+
+As an example, recall the definitions of `even` from
+Chapter [Relations](Relations).  
+\begin{code}
+data even : ℕ → Set where
+  ev0 : even zero
+  ev+2 : ∀ {n : ℕ} → even n → even (suc (suc n))
+\end{code}
+A number is even if it is zero, or if it is two
+greater than an even number.
+
+We will show that a number is even if and only if it is twice some
+other number.  That is, number `n` is even if and only if there exists
+a number `m` such that twice `m` is `n`.
+
+First, we need a lemma, which allows us to
+simplify twice the successor of `m` to two
+more than twice `m`.
+\begin{code}
+lemma : ∀ (m : ℕ) → 2 * suc m ≡ suc (suc (2 * m))
+lemma m =
+  begin
+    2 * suc m
+  ≡⟨⟩
+    suc m + (suc m + zero)
+  ≡⟨⟩
+    suc (m + (suc (m + zero)))
+  ≡⟨ cong suc (+-suc m (m + zero)) ⟩
+    suc (suc (m + (m + zero)))
+  ≡⟨⟩
+    suc (suc (2 * m))
+  ∎
+\end{code}
+The lemma is straightforward, and uses the lemma
+`+-suc` from Chapter [Properties](Properties), which
+allows us to simplify `m + suc n` to `suc (m + n)`.
+
+Here is the proof in the forward direction.
+\begin{code}  
+ev-ex : ∀ {n : ℕ} → even n → ∃(λ (m : ℕ) → 2 * m ≡ n)
+ev-ex ev0 =  (zero , refl)
+ev-ex (ev+2 ev) with ev-ex ev
+... | (m , refl) = (suc m , lemma m)
+\end{code}
+Given an even number, we must show it is twice some
+other number.  The proof is a function, which
+given a proof that `n` is even
+returns a pair consisting of `m` and a proof
+that twice `m` is `n`.  The proof is by induction over
+the evidence that `n` is even.
+
+- If the number is even because it is zero, then we return a pair
+consisting of zero and the (trivial) proof that twice zero is zero.
+
+- If the number is even because it is two more than another even
+number `n`, then we apply the induction hypothesis, giving us a number
+`m` and a proof that `2 * m ≡ n`, which we match against `refl`.  We
+return a pair consisting of `suc m` and a proof that `2 * suc m ≡ suc
+(suc n)`, which follows from `2 * m ≡ n` and the lemma.
+
+Here is the proof in the reverse direction.
+\begin{code}
+ex-ev : ∀ {n : ℕ} → ∃(λ (m : ℕ) → 2 * m ≡ n) → even n
+ex-ev (zero , refl) = ev0
+ex-ev (suc m , refl) rewrite lemma m = ev+2 (ex-ev (m , refl))
+\end{code}
+Given a number that is twice some other number,
+we must show that it is even.  The proof is a function,
+which given a number `m` and a proof that `n` is twice `m`,
+returns a proof that `n` is even.  The proof is by induction
+over the number `m`.
+
+- If it is zero, then we must show that twice zero is even,
+which follows by rule `ev0`. 
+
+- If it is `suc m`, then we must show that `2 * suc m` is
+even.  After rewriting with our lemma, we must show that
+`suc (suc (2 * m))` is even.  The inductive hypothesis tells
+us `2 * m` is even, from which the desired result follows
+by rule `ev+2`.
+
+Negation of an existential is isomorphic to universal
+of a negation.  Considering that existentials are generalised
+disjuntion and universals are generalised conjunction, this
+result is analogous to the one which tells us that negation
+of a disjuntion is isomorphic to a conjunction of negations.
+\begin{code}
 ¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃ (λ (x : A) → B x)) ≃ ∀ (x : A) → ¬ B x
 ¬∃∀ =
   record
@@ -1185,25 +1263,24 @@ extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fx
     ; invʳ =  λ { ∀¬bx → refl } 
     }
 \end{code}
+In the `to` direction, we are given a value `¬∃bx` of type
+`¬ ∃ (λ (x : A) → B x)`, and need to show that given a value
+`x` of type `A` that `¬ B x` follows, in other words, from
+a value `bx` of type `B x` we can derive false.  Combining
+`x` and `bx` gives us a value `(x , bx)` of type `∃ (λ (x : A) → B x)`,
+and applying `¬∃bx` to that yields a contradiction.
 
+In the `fro` direction, we are given a value `∀¬bx` of type
+`∀ (x : A) → ¬ B x`, and need to show that from a value `(x , bx)`
+of type `∃ (λ (x : A) → B x)` we can derive false.  Applying `∀¬bx`
+to `x` gives a value of type `¬ B x`, and applying that to `bx` yields
+a contradiction.
 
+The two inverse proofs are straightforward, where one direction
+requires extensionality.
 
-[It would be better to have even and odd as an exercise.  Is there
-a simpler example that I could start with?]
+*Exercise* Show `∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x)`.
 
-As an example, recall the definitions of `even` and `odd` from
-Chapter [Relations](Relations).  
-\begin{code}
-mutual
-  data even : ℕ → Set where
-    ev-zero : even zero
-    ev-suc : ∀ {n : ℕ} → odd n → even (suc n)
-  data odd : ℕ → Set where
-    od-suc : ∀ {n : ℕ} → even n → odd (suc n)
-\end{code}
-We show that a number `n` is even if and only if there exists
-another number `m` such that `n ≡ 2 * m`, and is odd if and only
-if there is another number `m` such that `n ≡ 1 + 2 * m`.
 
 
 ## Decidability
@@ -1214,9 +1291,6 @@ data Dec : Set → Set where
   no  : ∀ {A : Set} → (¬ A) → Dec A
 \end{code}
 
-## Equivalence
-
-
 ## Unicode
 
 This chapter introduces the following unicode.

src/LogicAns.lagda

@@ -9,6 +9,9 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
 open import Logic
 \end{code}
 
+
+*Equivalences for classical logic*
+
 \begin{code}
 ex1 : ¬¬-elim → excluded-middle
 ex1 h = h excluded-middle-irrefutable
@@ -46,3 +49,10 @@ help′ em ¬a×b with em | em
     ; invʳ =  λ { tt → refl }
     }
 \end{code}  
+
+*Existentials and Universals*
+
+\begin{code}
+∃¬¬∀ : ∀ {A : Set} {B : A → Set} → ∃ (λ (x : A) → ¬ B x) → ¬ (∀ (x : A) → B x)
+∃¬¬∀ (x , ¬bx) ∀bx = ¬bx (∀bx x)
+\end{code}

src/Properties.lagda

@@ -13,15 +13,13 @@ by their name, properties of *inductive datatypes* are proved by
 ## Imports
 
 Each chapter will begin with a list of the imports we require from the
-Agda standard library.
-
-<!-- We will, of course, require the naturals; everything in the
+Agda standard library.  We will, of course, require the naturals; everything in the
 previous chapter is also found in the library module `Data.Nat`, so we
 import the required definitions from there.  We also require
-propositional equality. -->
+propositional equality.
 
 \begin{code}
-open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
 \end{code}
 

src/Relations.lagda

@@ -10,8 +10,8 @@ the next step is to define relations, such as *less than or equal*.
 ## Imports
 
 \begin{code}
-open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_)
-open import Properties using (+-comm)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
+open import Data.Nat.Properties.Simple using (+-comm)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 \end{code}
 

src/extra/EvenOdd2.agda

@@ -0,0 +1,46 @@
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Product using (∃; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+
++-identity : ∀ (m : ℕ) → m + zero ≡ m
++-identity zero = refl
++-identity (suc m) rewrite +-identity m = refl
+
++-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
++-suc m zero = refl
++-suc m (suc n) rewrite +-suc m n = refl
+
++-comm : ∀ (m n : ℕ) → m + n ≡ n + m
++-comm zero n rewrite +-identity n = refl
++-comm (suc m) n rewrite +-suc m n | +-comm m n = refl
+
+data even : ℕ → Set
+data odd : ℕ → Set
+
+data even where
+  zero : even zero
+  suc : ∀ {n : ℕ} → odd n → even (suc n)
+data odd where
+  suc : ∀ {n : ℕ} → even n → odd (suc n)
+
++-lemma : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
++-lemma m rewrite +-identity m | +-suc m m = refl
+
+mutual
+  is-even : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
+  is-even zero zero =  zero , refl
+  is-even (suc n) (suc oddn) with is-odd n oddn
+  ... | m , n≡1+2*m rewrite n≡1+2*m | +-lemma m = suc m , refl
+
+  is-odd : ∀ (n : ℕ) → odd n → ∃(λ (m : ℕ) → n ≡ 1 + 2 * m)
+  is-odd (suc n) (suc evenn) with is-even n evenn
+  ... | m , n≡2*m rewrite n≡2*m = m , refl
+
++-lemma′ : ∀ (m : ℕ) → suc (suc (m + (m + 0))) ≡ suc m + suc (m + 0)
++-lemma′ m rewrite +-suc (m + 0) m = refl
+
+is-even′ : ∀ (n : ℕ) → even n → ∃(λ (m : ℕ) → n ≡ 2 * m)
+is-even′ zero zero =  zero , refl
+is-even′ (suc n) (suc oddn) with is-odd n oddn
+... | m , n≡1+2*m rewrite n≡1+2*m | +-identity m | +-suc m m = suc m , {!!}
+

src/extra/Isomorphisms.agda

@@ -0,0 +1,18 @@
+Extensionality of a function of two arguments
+
+\begin{code}
+extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
+extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
+\end{code}
+
+Isomorphism of all and exists.
+\begin{code}
+¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃ (λ (x : A) → B x)) ≃ ∀ (x : A) → ¬ B x
+¬∃∀ =
+  record
+    { to   =  λ { ¬∃bx x bx → ¬∃bx (x , bx) }
+    ; fro  =  λ { ∀¬bx (x , bx) → ∀¬bx x bx }
+    ; invˡ =  λ { ¬∃bx → extensionality (λ { (x , bx) → refl }) } 
+    ; invʳ =  λ { ∀¬bx → refl } 
+    }
+\end{code}

src/extra/Reasoning2.agda

@@ -0,0 +1,82 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans)
+open Eq.≡-Reasoning
+
+open import Data.Nat using (ℕ; zero; suc; _+_)
+
+lift : ∀ {m n : ℕ} → m ≡ n → suc m ≡ suc n
+lift refl = refl
+
++-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
++-assoc zero n p =
+  begin
+    (zero + n) + p
+  ≡⟨⟩
+    zero + (n + p)
+  ∎
++-assoc (suc m) n p =
+  begin
+    (suc m + n) + p
+  ≡⟨⟩
+    suc ((m + n) + p)
+  ≡⟨ lift (+-assoc m n p) ⟩
+    suc (m + (n + p))
+  ≡⟨⟩
+    suc m + (n + p)
+  ∎
+
++-identity : ∀ (m : ℕ) → m + zero ≡ m
++-identity zero =
+  begin
+    zero + zero
+  ≡⟨⟩
+    zero
+  ∎
++-identity (suc m) =
+  begin
+    suc m + zero
+  ≡⟨⟩
+    suc (m + zero)
+  ≡⟨ lift (+-identity m) ⟩
+    suc m
+  ∎
+
++-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
++-suc zero n =
+  begin
+    zero + suc n
+  ≡⟨⟩
+    suc n
+  ≡⟨⟩
+    suc (zero + n)
+  ∎
++-suc (suc m) n =
+  begin
+    suc m + suc n
+  ≡⟨⟩
+    suc (m + suc n)
+  ≡⟨ lift (+-suc m n) ⟩
+    suc (suc (m + n))
+  ≡⟨⟩
+    suc (suc m + n)
+  ∎
+
++-comm : ∀ (m n : ℕ) → m + n ≡ n + m
++-comm m zero =
+  begin
+    m + zero
+  ≡⟨ +-identity m ⟩
+    m
+  ≡⟨⟩
+    zero + m
+  ∎
++-comm m (suc n) =
+  begin
+    m + suc n
+  ≡⟨ +-suc m n ⟩
+    suc (m + n)
+  ≡⟨ lift (+-comm m n) ⟩
+    suc (n + m)
+  ≡⟨⟩
+    suc n + m
+  ∎

src/extra/extra.agda

@@ -0,0 +1,6 @@
+postulate
+  extensionality : ∀ {A B : Set} → {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
+
+extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
+extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
+

src/extra/outline.lagda

@@ -0,0 +1,142 @@
+Outline of
+Programming Languages Theory in Agda (PLTA)
+  [can I think of a wadlerian name?]
+
+
+Naturals
+  definition of naturals and why it makes sense
+    Nat; zero; suc
+Recursion
+  recursive definitions and why they make sense
+    _+_; _*_; _∸_
+  Exercises
+    _^_; _⊔_; _⊓_
+Induction
+  proof by induction and its relation to recursion
+    +-assoc; +-suc; +-identity; +-comm
+    *-distributes-+
+  classifying operations
+    associative; identity; commutative; distributive; idempotent
+    monoid; Abelian monoid; ring
+  Exercises
+    *-assoc; *-comm; ∸-+-assoc
+    ^-distributes-*; +-distributes-⊔; +-distributes-⊓
+    counterexamples to show that _^_ is not associative or commutative
+Relations
+  specifying relations by an inductive datatype
+  classifying relations
+    reflexive; symmetric; antisymmetric; transitive; total
+    preorder; partial order; total order
+    [do I also want irreflexive (requires negation)?]
+    [should I include a bit of lattice theory?]
+  proof by induction over evidence
+    ≤-refl; ≤-trans; ≤-antisym; ≤-total
+    [define ≤-total using ⊎ or a custom datatype? Probably custom is better]    
+  decidable relations
+    total order corresponds to a decidable relation
+Lists
+  definition
+    data List : Set → Set where
+      [] : ∀ {A : Set} → List A
+      _::_ : ∀ {A : Set} → A → List A → List A
+  equivalent way to write:
+    data List (A : Set) : Set where
+      [] : List A
+      _::_ : A → List A → List A
+  length
+  append _++_
+    infixr 5 _++_
+    ++-monoid
+  and or any all sum product
+  reverse
+    reverse and append
+    double reverse
+    fast and slow reverse and their equivalence
+    exercise : length xs ≡ length (reverse xs)
+  function composition
+  map
+    composition of two maps
+  foldr
+    composition of foldr with map
+  foldl
+    relation of foldr, foldl, and reverse
+  lexicographic order
+    define using a nested module
+    data Lex {a ℓ₁ ℓ₂} {A : Set a} (P : Set)
+             (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) : Rel (List A) (ℓ₁ ⊔ ℓ₂) where
+      base : P                             → Lex P _≈_ _≺_ []       []
+      halt : ∀ {y ys}                      → Lex P _≈_ _≺_ []       (y ∷ ys)
+      this : ∀ {x xs y ys} (x≺y : x ≺ y)   → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
+      next : ∀ {x xs y ys} (x≈y : x ≈ y)
+             (xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
+
+Logic
+  isomorphism
+    use two different definitions of ≤ as an example
+  projection
+    will get an example later, with ⊎-distributes-×
+  conjunction and top
+    ×-assoc; ×-comm; ×-ident (as isomorphisms)
+  disjunction and bottom
+    ⊥-elim
+    ⊎-assoc; ⊎-comm; ⊎-ident (as isomorphisms)
+  distributive laws
+    ×-distributes-⊎ (as isomorphism)
+      [The proof is straightforward but lengthy. Is there a way to shorten it?]
+    ⊎-distributes-× (as projection)
+  implication
+    reflexive and transitive
+  negation
+    contrapositive: (A → B) → (¬ B → ¬ A)
+    double negation introduction: A → ¬ ¬ A
+    triple negation elimination: ¬ ¬ ¬ A → ¬ A
+    excluded middle irrefutable: ¬ ¬ (A ⊎ ¬ A)
+  for all
+  there exists
+    example: even n → ∃(λ m → n = 2 * m)
+    exercise: odd n → ∃(λ m → n = 2 * m + 1)
+    example: 
+      ∀ (A : Set) (B : A → Set) → 
+        (∀ (x : A) → B x) → ¬ ∃ (λ (x : A) → ¬ B x)
+    exercise:
+      ∀ (A : Set) (B : A → Set) →
+        ∃ (λ (x : A) → B x) → ¬ (∀ (x : A) → ¬ B x)
+  intuitionistic and classical logic
+    following are all equivalent
+      excluded middle: A ⊎ ¬ A
+      double negation elimination: ¬ ¬ A → A
+      Peirce's law: ∀ (A B : Set) → ((A → B) → A) → A
+      de Morgan's law: ¬ (¬ A × ¬ B) → A ⊎ B
+      implication implies disjunction: (A → B) → ¬ A ⊎ B
+    show classical implies
+      ∀ (A : Set) (B : A → Set) → 
+        ¬ (∃(λ (x : A) → ¬ B x) → ∀ (x : A) → B x
+      ∀ (A : Set) (B : A → Set) →
+        ¬ (∀ (x : A) → ¬ B x) → ∃(λ (x : A) → B x)
+    [demonstrate Kolmogorov's or Gödel's embedding]
+  equivalence
+    how it is defined
+    biimplication with Leibniz equality
+
+Equivalence [not sure where this goes]
+  how it is defined
+  library for reasoning about it
+Lambda notation [don't know where to put this]
+  [Best if it comes *before* existentials]
+Currying [don't know where to put this]
+Structures [not sure where this goes]
+  [distribute as they are introduced, or centralise in one chapter?]
+  mathematical structures as records
+    equivalence
+    monoid; Abelian monoid; ring
+    preorder; partial order; total order
+    lattice
+    isomorphism; projection;
+    relation inclusion; biinclusion
+  other properties of relations
+    irreflexive
+    complement of a relation
+
+
+
+