revisions on Natural to Isomorphism

src/Equality.lagda

@@ -6,9 +6,8 @@ permalink : /Equality
 
 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,
-but in fact it can be defined using the machinery of inductive
-datatypes.
+are interchangeable.  So far we have treated equality as a primitive,
+but in fact it can be defined an an inductive datatype.
 
 
 ## Imports
@@ -198,11 +197,11 @@ 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
+We could replace any use of a chain of equations by a chain of
 applications of `trans`; the result would be more compact but harder
-to read.  The trick behind `∎` means that the chain always ends in the
-form `trans e refl`, where `e` proves some equation, even though `e`
-alone would do.
+to read.  The trick behind `∎` means that a chain of equalities simplifies
+to a chain of applications of `trans` than ends in `trans e refl`,
+where `e` is a term that proves some equality, even though `e` alone would do.
 
 
 ## Chains of equations, another example
@@ -348,7 +347,7 @@ hole causes it to be filled with `ev`.
 
 One may perform multiple rewrites, each separated by a vertical bar.  For instance,
 here is a second proof that addition is commutative, relying on rewrites rather
-than tabular reasoning.
+than chains of equalities.
 \begin{code}
 +-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
 +-comm′ zero n rewrite +-identity n = refl
@@ -358,8 +357,8 @@ This is far more compact.  Among other things, whereas the previous
 proof required `cong suc (+-comm m n)` as the justification to invoke the
 inductive hypothesis, here it is sufficient to rewrite with `+-comm m n`, as
 rewriting automatically takes congruence into account.  Although proofs
-with rewriting are shorter, proofs in tabular form make the reasoning
-involved easier to follow, and we will stick with the latter when feasible.
+with rewriting are shorter, proofs as chains of equalities are easier to follow,
+and we will stick with the latter when feasible.
 
 
 ## Rewriting expanded
@@ -495,3 +494,26 @@ by reflexivity of Martin Löf equivalence, and hence `Q y` follows from
 Isomorphic to Martin-Löf Identity, Parametrically*, by Andreas Abel,
 Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler,
 draft paper, 2017.)
+
+
+## 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_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+
+Here the import is shown as comment rather than code to avoid collisions,
+as mentioned in the introduction.
+
+
+## Unicode
+
+This chapter uses the following unicode.
+
+    ≡  U+2261  IDENTICAL TO (\==)  =
+    ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
+    ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
+    ∎  U+220E  END OF PROOF (\qed)
+    ≐  U+2250  APPROACHES THE LIMIT (\.=)

src/Isomorphism.lagda

@@ -24,10 +24,17 @@ open Eq.≡-Reasoning
 In set theory, two sets are isomorphic if they are in one-to-one correspondence.
 Here is the formal definition of isomorphism.
 \begin{code}
+record _InverseOf_ {A B : Set} (to : A → B) (from : B → A) : Set where
+  field
+    left-inverse-of  : ∀ (x : A) → from (to x) ≡ x
+    right-inverse-of : ∀ (y : B) → to (from y) ≡ y
+open _InverseOf_    
+
 record _≃_ (A B : Set) : Set where
   field
     to   : A → B
     from : B → A
+    -- inverse-of : to InverseOf from
     from∘to : ∀ (x : A) → from (to x) ≡ x
     to∘from : ∀ (y : B) → to (from y) ≡ y
 open _≃_ 
@@ -95,20 +102,23 @@ and `from` to be the identity function.
     ; to∘from = λ{y → refl}
     } 
 \end{code}
-This is our first use of *lambda expressions*.  A term of the form
+This is our first use of *lambda expressions*, provide a compact way to
+define functions without naming them.  A term of the form
 
-    λ{p → e}
+    λ{p₁ → e₁; ⋯ ; pᵢ → eᵢ}
     
-is equivalent to a function `f` defined by the equation
+is equivalent to a function `f` defined by the equations
 
-    f p = e
+    f p₁ = e₁
+    ⋯
+    f pᵢ = eᵢ
 
-where `p` is a pattern (left-hand side of an equation) and `e` is an expression
+where the `pᵢ` are patterns (left-hand sides of an equation) and the `eᵢ` are expressions
 (right-hand side of an equation).  Thus, 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`. The latter discard their arguments
-because the proofs are so straightforward that they are independent of the argument.
-That will not be the case for many of the later proofs.
+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)` simplifies to `x`, and similarly
+for the right inverse.
 
 To show isomorphism is symmetric, we simply swap the roles of `to`
 and `from`, and `from∘to` and `to∘from`.
@@ -117,7 +127,7 @@ and `from`, and `from∘to` and `to∘from`.
 ≃-sym A≃B =
   record
     { to      = from A≃B
-    ; from    = to A≃B
+    ; from    = to   A≃B
     ; from∘to = to∘from A≃B
     ; to∘from = from∘to A≃B
     }
@@ -128,7 +138,7 @@ equational reasoning to combine the inverses.
 ≃-trans : ∀ {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
 ≃-trans A≃B B≃C =
   record
-    { to       = λ{x → to B≃C (to A≃B x)}
+    { to       = λ{x → to   B≃C (to   A≃B x)}
     ; from     = λ{y → from A≃B (from B≃C y)}
     ; from∘to  = λ{x →
         begin
@@ -213,7 +223,7 @@ right inverses.
 ≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
 ≲-trans A≲B B≲C =
   record
-    { to      = λ{x → to B≲C (to A≲B x)}
+    { to      = λ{x → to   B≲C (to   A≲B x)}
     ; from    = λ{y → from A≲B (from B≲C y)}
     ; from∘to = λ{x →
         begin
@@ -278,4 +288,11 @@ open ≲-Reasoning
 \end{code}
 
 
+## Standard library
+
+Definitions similar to those in this chapter can be found in the standard library.
+\begin{code}
+-- import Function.Inverse using (Inverse; _↔_; to; from; inverse-of; left-inverse-of; right-inverse-of)
+-- import Function.LeftInverse using (LeftInverse; _↞_; to; from; left-inverse-of)
+\end{code}
 

src/Naturals.lagda

@@ -377,8 +377,8 @@ dummy name can be reused, and is convenient for examples.  Names other
 than `_` must be used only once in a module.
 
 Here the type is `2 + 3 ≡ 5` and the term provides *evidence* for the
-corresponding equation, here written as a chain of equations.  The
-chain starts with `begin` and finishes with `∎` (pronounced "qed" or
+corresponding equation, here written in tabular form as a chain of equations.
+The chain starts with `begin` and finishes with `∎` (pronounced "qed" or
 "tombstone", the latter from its appearance), and consists of a series
 of terms separated by `≡⟨⟩`.
 
@@ -415,7 +415,6 @@ other word for evidence, which we will use interchangeably, is *proof*.
 Compute `3 + 4`, writing out your reasoning as a chain of equations.
 
 
-
 ## Multiplication
 
 Once we have defined addition, we can define multiplication
@@ -466,10 +465,12 @@ and the third line matches the base case by taking `n = 3`.
 Here we have omitted the signature declaring `_ : 2 * 3 ≡ 6`, since
 it can easily be inferred from the corresponding term.
 
+
 ### Exercise (`3*4`)
 
 Compute `3 * 4`.
 
+
 ### Exercise (`_^_`).
 
 Define exponentiation, which is given by the following equations.
@@ -824,18 +825,20 @@ former on `ℕ`, and the latter on the equivalent type `Data.Nat.ℕ`.
 Such a pragma can only be invoked once, as invoking it twice would
 raise confusion as to whether `2` is a value of type `ℕ` or type
 `Data.Nat.ℕ`.  Similar confusions arise if other pragmas are invoked
-twice. For this reason, we will not invoke pragmas in future chapters,
-leaving that to the standard library. Information on available
-pragmas can be found in the Agda documentation.
+twice. For this reason, we will usually avoid pragmas in future chapters.
+Information on pragmas can be found in the Agda documentation.
 
 
 ## Unicode
 
-This chapter introduces the following unicode.
+This chapter uses the following unicode.
 
     ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)  
     →  U+2192  RIGHTWARDS ARROW (\to, \r)
     ∸  U+2238  DOT MINUS (\.-)
+    ≡  U+2261  IDENTICAL TO (\==)  =
+    ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
+    ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
     ∎  U+220E  END OF PROOF (\qed)
 
 Each line consists of the Unicode character (`ℕ`), the corresponding

src/Properties.lagda

@@ -755,9 +755,8 @@ import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)
 
 ## Unicode
 
-This chapter introduces the following unicode.
+This chapter uses the following unicode.
 
-    ≡  U+2261  IDENTICAL TO (\==)
     ∀  U+2200  FOR ALL (\forall)
     ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
     ′  U+2032  PRIME (\')

src/Relations.lagda

@@ -13,7 +13,6 @@ the next step is to define relations, such as *less than or equal*.
 \begin{code}
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
 open import Data.Nat.Properties using (+-comm; +-suc)
 \end{code}
@@ -616,12 +615,13 @@ make implicit arguments that here are explicit.
 
 ## Unicode
 
-This chapter introduces the following unicode.
+This chapter uses the following unicode.
 
     ≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
     ≥  U+2265  GREATER-THAN OR EQUAL TO (̄\>=, \ge)
     ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)
+    ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
 
-Similar to `\^r`, the command `\^l` gives access to a variety of
-superscript leftward arrows, and also a superscript letter `l`.
+The commands `\^l` and `\^r` give access to a variety of superscript
+leftward and rightward arrows, and also superscript letters `l` and `r`.