rewritten as requested by @wadler

Author: peterthiemann

src/plfa/part1/Isomorphism.lagda.md

@@ -392,7 +392,8 @@ are cut down versions of the similar proofs for isomorphism:
 
 It is also easy to see that if two types embed in each other, and the
 embedding functions correspond, then they are isomorphic.  This is a
-weak form of anti-symmetry:
+weak form of anti-symmetry.  The proof does some of the work by
+matching the evidence that the functions correspond against `refl`:
 
 ```agda
 ≲-antisym : ∀ {A B : Set}
@@ -402,43 +403,7 @@ weak form of anti-symmetry:
   → (from A≲B ≡ to B≲A)
     -------------------
   → A ≃ B
-≲-antisym A≲B B≲A to≡from from≡to =
-  record
-    { to      = to A≲B
-    ; from    = from A≲B
-    ; from∘to = from∘to A≲B
-    ; to∘from = λ{y →
-        begin
-          to A≲B (from A≲B y)
-        ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
-          to A≲B (to B≲A y)
-        ≡⟨ cong-app to≡from (to B≲A y) ⟩
-          from B≲A (to B≲A y)
-        ≡⟨ from∘to B≲A y ⟩
-          y
-        ∎}
-    }
-```
-
-The first three components are copied from the embedding, while the
-last combines the left inverse of `B ≲ A` with the equivalences of
-the `to` and `from` components from the two embeddings to obtain
-the right inverse of the isomorphism.
-
-The previous proof can also be shortened by doing more work in the
-patterns on the left-hand side.  If the two proofs that the embedding
-functions correspond are both matched against `refl`, then Agda records
-that the corresponding functions are the same:
-
-```agda
-≲-antisym′ : ∀ {A B : Set}
-  → (A≲B : A ≲ B)
-  → (B≲A : B ≲ A)
-  → (to A≲B ≡ from B≲A)
-  → (from A≲B ≡ to B≲A)
-    -------------------
-  → A ≃ B
-≲-antisym′ A≲B B≲A refl refl =
+≲-antisym A≲B B≲A to≡from@refl from≡to@refl =
   record
     { to      = to A≲B
     ; from    = from A≲B
@@ -447,35 +412,46 @@ that the corresponding functions are the same:
     }
 ```
 
-After matching the third parameter, called `to≡from` above, against
-`refl`, Agda knows that `to A≲B` and `from B≲A` are the same function.
-After matching the fourth parameter, called `from≡to` above, against
-`refl`, Agda knows that `from A≲B` and `to B≲A` are the same function.
-Hence the type of `from∘to B≲A`,
-
-    ∀ (y : B) → from B≲A (to B≲A y) ≡ y
-
-is the same as the type required for `to∘from`,
-
-    ∀ (y : B) → to A≲B (from A≲B y) ≡ y.
+The first three components are copied from the embedding `A≲B`.  For
+the last component, matching `to≡from` against `refl` tells Agda that
+`to A≲B` and `from B≲A` are the same function, while matching
+`from≡to` against `refl` tells Agda that `from A≲B` and `to B≲A` are
+the same function.  Hence `from∘to B≲A` has the required type.
 
 One subtlety is why Agda accepts these `refl` patterns at all.  The
 equalities compare projections from two records, rather than variables
 written directly on the left-hand side.  Agda silently η-expands record
 values.  This property is called η-equality for records: a record is
-determined by its fields.  A value `A≲B` is definitionally the same as
-the record obtained by projecting out all its fields and putting them
-back together.  For an embedding, this means `A≲B` is the same as
+determined by its fields.  A record value is definitionally equal to the
+record obtained by projecting out all its fields and putting them back
+together.  Thus, when checking the left-hand side, Agda may view the two
+embeddings as
 
     record
-      { to      = to A≲B
-      ; from    = from A≲B
-      ; from∘to = from∘to A≲B
+      { to      = f
+      ; from    = g
+      ; from∘to = p
       }
 
-and similarly for `B≲A`.  This η-expansion lets pattern matching on
-`refl` refine the corresponding record fields, which is why the shorter
-proof can replace the whole equational derivation by `from∘to B≲A`.
+and
+
+    record
+      { to      = h
+      ; from    = k
+      ; from∘to = q
+      }
+
+where `f` is `to A≲B`, `g` is `from A≲B`, `h` is `to B≲A`, and `k` is
+`from B≲A`.  After this expansion, the equality arguments have types
+`f ≡ k` and `g ≡ h`, so matching them against `refl` identifies
+`f` with `k`, and `g` with `h`.  It is not that η-expanding `A≲B`
+computes `to A≲B` to something new; rather, η-expansion lets Agda
+expose the fields of record variables while solving the pattern match.
+Under these identifications, `from∘to B≲A` has type
+
+    ∀ (y : B) → to A≲B (from A≲B y) ≡ y
+
+which is exactly the type required for `to∘from`.
 
 # Equational reasoning for embedding