completed pass over Equality

src/Equality.lagda

@@ -4,9 +4,6 @@ layout    : page
 permalink : /Equality
 ---
 
-<!-- TODO: Consider changing `Equivalence` to `Equality` or `Identity`.
-Possibly introduce the name `Martin Löf Identity` early on. -->
-
 Much of our reasoning has involved equality.  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,
@@ -31,8 +28,8 @@ open import Agda.Primitive using (Level; lzero; lsuc)
 
 We declare equivality as follows.
 \begin{code}
-data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
+data _≡_ {A : Set} : A → A → Set where
-  refl : x ≡ x
+  refl : ∀ {x : A} → 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
@@ -61,7 +58,7 @@ An equivalence relation is one which is reflexive, symmetric, and transitive.
 Reflexivity is built-in to the definition of equivalence, via the
 constructor `refl`.  It is straightforward to show symmetry.
 \begin{code}
-sym : ∀ {ℓ} {A : Set ℓ} {x y : A} →  x ≡ y → y ≡ x
+sym : ∀ {A : Set} {x y : A} →  x ≡ y → y ≡ x
 sym refl = refl
 \end{code}
 How does this proof work? The argument to `sym` has type `x ≡ y`,
@@ -112,7 +109,7 @@ This completes the definition as given above.
 
 Transitivity is equally straightforward.
 \begin{code}
-trans : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans refl refl = refl
 \end{code}
 Again, a useful exercise is to carry out an interactive development, checking
@@ -121,14 +118,14 @@ instantiated.
 
 ## Congruence and Substitution
 
-Equality also satisfies *congruence*.  If two terms are equal,
+Equality satisfies *congruence*.  If two terms are equal,
 they remain so after the same function is applied to both.
 \begin{code}
-cong : ∀ {ℓ} {A B : Set ℓ} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
+cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
 cong f refl = refl
 \end{code}
-Once more, a useful exercise is to carry out an interactive development.
 
+Equality also satisfies *substitution*.
 If two values are equal and a predicate holds of the first then it also holds of the second.
 \begin{code}
 subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
@@ -136,14 +133,14 @@ subst P refl px = px
 \end{code}
 
 
-## Tabular reasoning
+## Chains of equations
 
-Here we show how to support the form of tabular reasoning
+Here we show how to support reasoning with chains of equations
-we have used throughout the book.  We package the declarations
+as used throughout the book.  We package the declarations
 into a module, named `≡-Reasoning`, to match the format used in Agda's
 standard library.
 \begin{code}
-module ≡-Reasoning {ℓ} {A : Set ℓ} where
+module ≡-Reasoning {A : Set} where
 
   infix  1 begin_
   infixr 2 _≡⟨⟩_ _≡⟨_⟩_
@@ -166,11 +163,11 @@ open ≡-Reasoning
 Opening the module makes all of the definitions
 available in the current environment.
 
-As a simple example, let's look at the proof of transitivity
+As an example, let's look at a proof of transitivity
-rewritten in tabular form.
+as a chain of equations.
 \begin{code}
-trans′ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans′ : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-trans′ {ℓ} {A} {x} {y} {z} x≡y y≡z =
+trans′ {A} {x} {y} {z} x≡y y≡z =
   begin
     x
   ≡⟨ x≡y ⟩
@@ -179,7 +176,7 @@ trans′ {ℓ} {A} {x} {y} {z} x≡y y≡z =
     z
   ∎
 \end{code}
-According to the fixity declarations, the body parses as follows.
+According to the fixity declarations, the body parses as follows:
 
     begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))
 
@@ -195,21 +192,20 @@ third arguments are both proofs of equations, in particular proofs of
 `y ≡ z` and `z ≡ z` respectively, which are combined by `trans` in the
 body of `_≡⟨_⟩_` to yield a proof of `y ≡ z`.  Finally, the proof of
 `z ≡ z` consists of `_∎` applied to the term `z`, which yields `refl`.
-After simplification, the body is equivalent to the following term.
+After simplification, the body is equivalent to the term:
 
     trans x≡y (trans y≡z refl)
 
 We could replace all uses of tabular reasoning by a chain of
-applications of `trans`; the result would be more compact but harder to read.
+applications of `trans`; the result would be more compact but harder
-Also note that the syntactic trick behind `∎` means that the chain
+to read.  The trick behind `∎` means that the chain always ends in the
-always ends in the form `trans e refl`, where `e` proves some equation,
+form `trans e refl`, where `e` proves some equation, even though `e`
-even though `e` alone would do.
+alone would do.
 
-<!--
 
-## Tabular reasoning, another example
+## Chains of equations, another example
 
-As a second example of tabular reasoning, we consider the proof that addition
+As a second example of chains of equations, we repeat the proof that addition
 is commutative.  We first repeat the definitions of naturals and addition.
 We cannot import them because (as noted at the beginning of this chapter)
 it would cause a conflict.
@@ -230,7 +226,6 @@ postulate
   +-identity : ∀ (m : ℕ) → m + zero ≡ m
   +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
 
-{-
 +-comm : ∀ (m n : ℕ) → m + n ≡ n + m
 +-comm m zero =
   begin
@@ -250,9 +245,8 @@ postulate
   ≡⟨⟩
     suc n + m
   ∎
--}
 \end{code}
-The tabular reasoning here is similar to that in the
+The reasoning here is similar to that in the
 preceding section, the one addition being the use of
 `_≡⟨⟩_`, which we use when no justification is required.
 One can think of occurrences of `≡⟨⟩` as an equivalent
@@ -274,19 +268,24 @@ the lines and write
       suc (n + m)
 
 and Agda would not object. Agda only checks that the terms
-separated by `≡⟨⟩` are equivalent; it's up to us to write
+separated by `≡⟨⟩` have the same simplified form; it's up to us to write
 them in an order that will make sense to the reader.
 
--->
 
 ## Rewriting
 
 Consider a property of natural numbers, such as being even.
-
+We repeat the earlier definition.
 \begin{code}
-data even : ℕ → Set where
+data even : ℕ → Set
-  ev0 : even zero
+data odd  : ℕ → Set
-  ev+2 : ∀ {n : ℕ} → even n → even (suc (suc n))
+
+data even where
+  even-zero : even zero
+  even-suc  : ∀ {n : ℕ} → odd n → even (suc n)
+
+data odd where
+  odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)
 \end{code}
 In the previous section, we proved addition is commutative.
 Given evidence that `even (m + n)` holds,
@@ -303,9 +302,6 @@ corresponds to equivalence.
 
 We can then prove the desired property as follows.
 \begin{code}
-postulate
-  +-comm : ∀ (m n : ℕ) → m + n ≡ n + m
-
 even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m)
 even-comm m n ev rewrite +-comm m n = ev
 \end{code}
@@ -375,16 +371,24 @@ even-comm′ m n ev with   m + n  | +-comm m n
 \end{code}
 The first clause asserts that `m + n` and `n + m` are identical, and
 the second clause justifies that assertion with evidence of the
-appropriate equivalence.  Note the use of the "dot pattern" `.(n +
+appropriate equivalence.  Note the use of the "dot pattern", `.(n + m)`.
-m)`.  A dot pattern is followed by an expression and is made when
+A dot pattern is followed by an expression and is made when
-other information allows one to identify the expession in the `with`
+other information forces the value matched to be equal to the value of
-clause with the expression it matches against.  In this case, the
+the expression in the dot pattern.  In this case, the identification
-identification of `m + n` and `n + m` is justified by the subsequent
+of `m + n` and `n + m` is justified by the subsequent matching of
-matching of `+-comm m n` against `refl`.  One might think that the
+`+-comm m n` against `refl`.  One might think that the first clause is
-first clause is redundant as the information is inherent in the second
+redundant as the information is inherent in the second clause, but in
-clause, but in fact Agda is rather picky on this point: omitting the
+fact Agda is rather picky on this point: omitting the first clause or
-first clause or reversing the order of the clauses will cause Agda to
+reversing the order of the clauses will cause Agda to report an error.
-report an error.  (Try it and see!)
+(Try it and see!)
+
+In this case, we can avoid rewrite by simply applying substitution.
+\begin{code}
+even-comm″ : ∀ (m n : ℕ) → even (m + n) → even (n + m)
+even-comm″ m n  =  subst even (+-comm m n)
+\end{code}
+Nonetheless, rewrite is a vital part of the Agda toolkit,
+as earlier examples have shown.
 
 
 ## Leibniz equality
@@ -407,20 +411,32 @@ holds of `y` also holds of `x`.
 Let `x` and `y` be objects of type $A$. We say that `x ≐ y` holds if
 for every predicate $P$ over type $A$ we have that `P x` implies `P y`.
 \begin{code}
-_≐_ : ∀ {ℓ} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
+_≐_ : ∀ {A : Set} (x y : A) → Set₁
-_≐_ {ℓ} {A} x y = (P : A → Set ℓ) → P x → P y
+_≐_ {A} x y = ∀ (P : A → Set) → P x → P y
 \end{code}
-Here we must make use of levels: if `A` is a set at level `ℓ` and `x` and `y`
+One might expect to write the left-hand side of the equation as `x ≐ y`,
-are two values of type `A` then `x ≐ y` is at the next level `lsuc ℓ`.
+but instead we write `_≐_ {A} x y` to provide access to the implicit
+parameter `A` which appears on the right-hand side.
+
+This is our first use of *levels*.  We cannot assign `Set` the type
+`Set`, since this would lead to contradictions such as Russel's
+Paradox and Girard's Paradox.  Instead, there is a hierarchy of types,
+where `Set : Set₁`, `Set₁ : Set₂`, and so on.  In fact, `Set` itself
+is just an abbreviation for `Set₀`.  Since the equation defining `_≐_`
+mentions `Set` on the right-hand side, the corresponding signature
+must use `Set₁`.  Further information on levels can be found in
+the [Agda Wiki][wiki].
+
+[wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
 
 Leibniz equality is reflexive and transitive,
 where the first follows by a variant of the identity function
 and the second by a variant of function composition.
 \begin{code}
-refl-≐ : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≐ x
+refl-≐ : ∀ {A : Set} {x : A} → x ≐ x
 refl-≐ P Px  =  Px
 
-trans-≐ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
+trans-≐ : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
 trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)
 \end{code}
 
@@ -433,10 +449,10 @@ implies `P x`.  The property `Q x` is trivial by reflexivity, and
 hence `Q y` follows from `x ≐ y`.  But `Q y` is exactly a proof of
 what we require, that `P y` implies `P x`.
 \begin{code}
-sym-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → y ≐ x
+sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
-sym-≐ {ℓ} {A} {x} {y} x≐y P  =  Qy
+sym-≐ {A} {x} {y} x≐y P  =  Qy
   where
-    Q : A → Set ℓ
+    Q : A → Set
     Q z = P z → P x
     Qx : Q x
     Qx = refl-≐ P
@@ -450,24 +466,22 @@ Leibniz equality, and vice versa.  In the forward direction, if we know
 which is easy since equivalence of `x` and `y` implies that any proof
 of `P x` is also a proof of `P y`.
 \begin{code}
-≡-implies-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x ≐ y
+≡-implies-≐ : ∀ {A : Set} {x y : A} → x ≡ y → x ≐ y
-≡-implies-≐ refl P Px = Px
+≡-implies-≐ x≡y P = subst P x≡y
 \end{code}
-The function `≡-implies-≐` is often called *substitution* because it
+This direction follows from substitution, which we showed earlier.
-says that if we know `x ≡ y` then we can substitute `y` for `x`,
-taking a proof of `P x` to a proof  of `P y` for any property `P`.
 
 In the reverse direction, given that for any `P` we can take a proof of `P x`
 to a proof of `P y` we need to show `x ≡ y`. The proof is similar to that
-for symmetry of Leibniz equality. We take $Q$
+for symmetry of Leibniz equality. We take `Q`
 to be the predicate that holds of `z` if `x ≡ z`. Then `Q x` is trivial
 by reflexivity of Martin Löf equivalence, and hence `Q y` follows from
 `x ≐ y`.  But `Q y` is exactly a proof of what we require, that `x ≡ y`.
 \begin{code}
-≐-implies-≡ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → x ≡ y
+≐-implies-≡ : ∀ {A : Set} {x y : A} → x ≐ y → x ≡ y
-≐-implies-≡ {ℓ} {A} {x} {y} x≐y = Qy
+≐-implies-≡ {A} {x} {y} x≐y = Qy
   where
-    Q : A → Set ℓ
+    Q : A → Set
     Q z = x ≡ z
     Qx : Q x
     Qx = refl

src/Naturals.lagda

@@ -393,24 +393,10 @@ check it is the same as `5`.  A binary relation is said to be *reflexive* if
 it holds between a value and itself.  Evidence that a value is equal to
 itself is written `refl`.
 
-In the chains of equations, all Agda checks is that each of the terms
+In the chains of equations, all Agda checks is that each term
 simplifies to the same value. If we jumble the equations, omit lines, or
-add extraneous lines it will still be accepted.
+add extraneous lines it will still be accepted.  It's up to us to write
-\begin{code}
+the equations in an order that makes sense to the reader.
-_ : 2 + 3 ≡ 5
-_ =
-  begin
-    2 + 3
-  ≡⟨⟩
-    4 + 1
-  ≡⟨⟩
-    5
-  ≡⟨⟩
-    suc (suc (0 + 3))
-  ∎
-\end{code}
-Of course, writing a proof in this way would be misleading and confusing,
-so it's to be avoided even if Agda does accept it.
 
 Here `2 + 3 ≡ 5` is a type, and the chains of equations (and also
 `refl`) are terms of the given type; alternatively, one can think of