moved def'n of lambda from Isomorphism to Equality

src/Equality.lagda

@@ -400,6 +400,43 @@ Nonetheless, rewrite is a vital part of the Agda toolkit,
 as earlier examples have shown.
 
 
+## Lambda expressions
+
+We pause for a moment to define *lambda expressions*, which provide a
+compact way to define functions without naming them, and will prove
+convenient in much of what follows.
+
+A term of the form
+
+    λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ }
+    
+is equivalent to a function `f` defined by the equations
+
+    f P₁ = e₁
+    ⋯
+    f Pᵢ = eᵢ
+
+where the `Pᵢ` are patterns (left-hand sides of an equation) and the
+`Nᵢ` are expressions (right-hand side of an equation).
+
+In the case that the pattern is a variable, we may also use the syntax
+
+    λ x → N
+
+or
+
+    λ (x : A) → N
+
+both of which are equivalent to `λ{ x → N }`. The latter allows one to
+specify the domain of the function.
+
+Often using an anonymous lambda expression is more convenient than
+using a named function: it avoids a lengthy type declaration; and the
+definition appears exactly where the function is used, so there is no
+need for the writer to remember to declare it in advance, or for the
+reader to search for the definition elsewhere in the code.
+
+
 ## Extensionality {#extensionality}
 
 Extensionality asserts that the only way to distinguish functions is
@@ -606,11 +643,11 @@ term that includes `Set ℓ`.
 ## Standard library
 
 Definitions similar to those in this chapter can be found in the standard library.
-
-    import Relation.Binary.PropositionalEquality as Eq
-    open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-    open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
-
+\begin{code}
+-- import Relation.Binary.PropositionalEquality as Eq
+-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
+-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+\end{code}
 Here the import is shown as comment rather than code to avoid collisions,
 as mentioned in the introduction.
 
@@ -619,9 +656,10 @@ as mentioned in the introduction.
 
 This chapter uses the following unicode.
 
-    ≡  U+2261  IDENTICAL TO (\==)  =
+    ≡  U+2261  IDENTICAL TO (\==)
     ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
     ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
     ∎  U+220E  END OF PROOF (\qed)
+    λ  U+03BB  GREEK SMALL LETTER LAMBDA (\lambda, \Gl)
     ≐  U+2250  APPROACHES THE LIMIT (\.=)
     ℓ  U+2113  SCRIPT SMALL L (\ell)

src/Isomorphism.lagda

@@ -109,35 +109,10 @@ and `from` to be the identity function.
     ; to∘from = λ{y → refl}
     } 
 \end{code}
-This is our first use of *lambda expressions*, which provide a compact way to
-define functions without naming them.  A term of the form
-
-    λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ }
-    
-is equivalent to a function `f` defined by the equations
-
-    f P₁ = e₁
-    ⋯
-    f Pᵢ = eᵢ
-
-where the `Pᵢ` are patterns (left-hand sides of an equation) and the
-`Nᵢ` are expressions (right-hand side of an equation).  In the case that
-the pattern is a variable, we may also use the syntax
-
-    λ (x : A) → N
-
-which is equivalent to `λ{ x → N }` but allows one to specify the
-domain of the function. Often using an anonymous lambda expression is
-more convenient than using a named function: it avoids a lengthy type
-declaration; and the definition appears exactly where the function is
-used, so there is no need for the writer to remember to declare it in
-advance, or for the reader to search for the definition elsewhere in
-the code.
-
 In the above, `to` and `from` are both bound to identity functions,
 and `from∘to` and `to∘from` are both bound to functions that discard
 their argument and return `refl`.  In this case, `refl` alone is an
-adequate proof since for the left inverse, `λ{y → y} (λ{x → x} x)`
+adequate proof since for the left inverse, `to (from x)`
 simplifies to `x`, and similarly for the right inverse.
 
 To show isomorphism is symmetric, we simply swap the roles of `to`
@@ -319,8 +294,9 @@ import Function.Inverse using (_↔_)
 import Function.LeftInverse using (_↞_)
 \end{code}
 Here `_↔_` corresponds to our `_≃_`, and `_↞_` corresponds to our `_≲_`.
-However, we stick with the definitions given here, mainly because `_↔_` is
-specified as a nested record, rather than the flat records used here.
+However, we stick with our definitions, because those in the
+standard library are less convenient to use: they use a nested record structure,
+and are parameterised with regard to an arbitrary notion of equivalence.
 
 ## Unicode
 
@@ -328,4 +304,3 @@ This chapter uses the following unicode.
 
     ≃  U+2243  ASYMPTOTICALLY EQUAL TO (\~-)
     ≲  U+2272  LESS-THAN OR EQUIVALENT TO (\<~)
-    λ  U+03BB  GREEK SMALL LETTER LAMBDA (\lambda, \Gl)