factored out Isomorphism, Logic broken

index.md

@@ -23,12 +23,14 @@ http://homepages.inf.ed.ac.uk/wadler/
 
   - [Naturals: Natural numbers](Naturals)
   - [Properties: Proof by induction](Properties)
-  - [PropertiesAns: Solutions to exercises](PropertiesAns)
   - [Relations: Inductive Definition of Relations](Relations)
-  - [RelationsAns: Solutions to exercises](RelationsAns)
-  - [Logic: Logic](Logic)
-  - [LogicAns: Solutions to exercises](LogicAns)
   - [Equivalence: Equivalence and equational reasoning](Equivalence)
+  - [Isomorphism: Isomorphism and embedding](Isomorphism)
+  - [Logic: Logic](Logic)
+
+  - [PropertiesAns: Solutions to exercises](PropertiesAns) 
+  - [RelationsAns: Solutions to exercises](RelationsAns) 
+  - [LogicAns: Solutions to exercises](LogicAns)
 
 ## Part 2: Programming Language Foundations
 

src/Equivalence.lagda

@@ -4,6 +4,9 @@ layout    : page
 permalink : /Equivalence
 ---
 
+<!-- TODO: Consider changing `Equivalence` to `Equality` or `Identity`.
+Possibly introduce the name `Martin Löf Identity` early on. -->
+
 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,
@@ -13,10 +16,15 @@ datatypes.
 
 ## Imports
 
-This chapter has no imports.  Pretty much every module in the Agda
+Pretty much every module in the Agda
 standard library, and every chapter in this book, imports the standard
-definition of equivalence. Since we define equivalence here, any
+definition of equivalence. Since we define equivalence here, any such
-import would create a conflict.
+import would create a conflict.  The only import we make is the
+definition of type levels, which is so primitive that it precedes
+the definition of equivalence.
+\begin{code}
+open import Agda.Primitive using (Level; lzero; lsuc)
+\end{code}
 
 
 ## Equivalence
@@ -27,10 +35,12 @@ 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
+constructor `refl` provides evidence that `x ≡ x`. Hence, every value
-value is equivalent to itself, and we have no other way of showing values
+is equivalent to itself, and we have no other way of showing values
-are equivalent.  Here we have quantified over all levels, so that
+are equivalent.  We have quantified over all levels, so that we can
-we can apply equivalence to types belonging to any level.
+apply equivalence to types belonging to any level.  The definition
+features an asymetry, in that the first argument to `_≡_` is given by
+the parameter `x : A`, while the second is given by `A → Set ℓ`.
 
 We declare the precedence of equivalence as follows.
 \begin{code}
@@ -364,4 +374,92 @@ report an error.  (Try it and see!)
 ## Leibniz equality
 
 The form of asserting equivalence that we have used is due to Martin Löf,
-and was introduced in the 1970s.  
+and was published in 1975.  An older form is due to Leibniz, and was published
+in 1686.  Leibniz asserted the *identity of indiscernibles*: two objects are
+equal if and only if they satisfy the same properties. This
+principle sometimes goes by the name Leibniz' Law, and is closely
+related to Spock's Law, ``A difference that makes no difference is no
+difference''.  Here we define Leibniz equality, and show that two terms
+satsisfy Lebiniz equality iff and only if they satisfy Martin Löf equivalence.
+
+Leibniz equality is usually formalized to state that `x ≐ y`
+holds if every property `P` that holds of `x` also holds of
+`y`.  Perhaps surprisingly, this definition is
+sufficient to also ensure the converse, that every property `P` that
+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} 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`
+are two values of type `A` then `x ≐ y` is at the next level `lsuc ℓ`.
+
+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-≐ P Px = Px
+
+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}
+
+Symmetry is less obvious.  We have to show that if `P x` implies `P y`
+for all predicates `P`, then the implication holds the other way round
+as well.  Given a specific `P` and a proof `Py` of `P y`, we have to
+construct a proof of `P x` given `x ≐ y`.  To do so, we instantiate
+the equality with a predicate `Q` such that `Q z` holds if `P z`
+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} {x} {y} x≐y P = Qy
+  where
+    Q : A → Set ℓ
+    Q z = P z → P x
+    Qx : Q x
+    Qx = refl-≐ P
+    Qy : Q y
+    Qy = x≐y Q Qx
+\end{code}
+
+We now show that Martin Löf equivalence implies
+Leibniz equality, and vice versa.  In the forward direction, if we know
+`x ≡ y` we need for any `P` to take evidence of `P x` to evidence of `P y`,
+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-≐ refl P Px = Px
+\end{code}
+The function `≡-implies-≐` is often called *substitution* because it
+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$
+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} {x} {y} x≐y = Qy
+  where
+    Q : A → Set ℓ
+    Q z = x ≡ z
+    Qx : Q x
+    Qx = refl
+    Qy : Q y
+    Qy = x≐y Q Qx
+\end{code}
+
+(Parts of this section are adapted from *≐≃≡: Leibniz Equality is
+Isomorphic to Martin-Löf Identity, Parametrically*, by Andreas Abel,
+Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler,
+draft paper, 2017.)

src/Isomorphism.lagda

@@ -0,0 +1,242 @@
+---
+title     : "Isomorphism: Isomorphism and Embedding"
+layout    : page
+permalink : /Isomorphism
+---
+
+## 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
+
+As a prelude, we begin by introducing the notion of isomorphism.
+In set theory, two sets are isomorphism if they are in 1-to-1 correspondence.
+Here is the formal definition of isomorphism.
+\begin{code}
+record _≃_ (A B : Set) : Set where
+  field
+    to : A → B
+    fro : B → A
+    invˡ : ∀ (x : A) → fro (to x) ≡ x
+    invʳ : ∀ (y : B) → to (fro y) ≡ y
+open _≃_
+\end{code}
+Let's unpack the definition. An isomorphism between sets `A` and `B` consists
+of four things:
++ A function `to` from `A` to `B`,
++ A function `fro` from `B` back to `A`,
++ Evidence `invˡ` asserting that `to` followed by `from` is the identity,
++ Evidence `invʳ` asserting that `from` followed by `to` is the identity.
+The declaration `open _≃_` makes avaialable the names `to`, `fro`,
+`invˡ`, and `invʳ`, otherwise we would need to write `_≃_.to` and so on.
+
+The above is our first example of a record declaration. It is equivalent
+to a corresponding inductive data declaration.
+\begin{code}
+data _≃′_ : Set → Set → Set where
+  mk-≃′ : ∀ {A B : Set} →
+         ∀ (to : A → B) →
+         ∀ (fro : B → A) → 
+         ∀ (invˡ : (∀ (x : A) → fro (to x) ≡ x)) →
+         ∀ (invʳ : (∀ (y : B) → to (fro y) ≡ y)) →
+         A ≃′ B
+
+to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
+to′ (mk-≃′ f g gfx≡x fgy≡y) = f
+
+fro′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
+fro′ (mk-≃′ f g gfx≡x fgy≡y) = g
+
+invˡ′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → fro′ A≃B (to′ A≃B x) ≡ x)
+invˡ′ (mk-≃′ f g gfx≡x fgy≡y) = gfx≡x
+
+invʳ′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (fro′ A≃B y) ≡ y)
+invʳ′ (mk-≃′ f g gfx≡x fgy≡y) = fgy≡y
+\end{code}
+We construct values of the record type with the syntax:
+
+    record
+      { to = f
+      ; fro = g
+      ; invˡ = gfx≡x
+      ; invʳ = fgy≡y
+      }
+
+which corresponds to using the constructor of the corresponding
+inductive type:
+
+    mk-≃′ f g gfx≡x fgy≡y
+
+where `f`, `g`, `gfx≡x`, and `fgy≡y` are values of suitable types.
+      
+Isomorphism is an equivalence, meaning that it is reflexive, symmetric,
+and transitive.  To show isomorphism is reflexive, we take both `to`
+and `fro` to be the identity function.
+\begin{code}
+≃-refl : ∀ {A : Set} → A ≃ A
+≃-refl =
+  record
+    { to = λ x → x
+    ; fro = λ y → y
+    ; invˡ = λ x → refl
+    ; invʳ = λ y → refl
+    } 
+\end{code}
+To show isomorphism is symmetric, we simply swap the roles of `to`
+and `fro`, and `invˡ` and `invʳ`.
+\begin{code}
+≃-sym : ∀ {A B : Set} → A ≃ B → B ≃ A
+≃-sym A≃B =
+  record
+    { to = fro A≃B
+    ; fro = to A≃B
+    ; invˡ = invʳ A≃B
+    ; invʳ = invˡ A≃B
+    }
+\end{code}
+To show isomorphism is transitive, we compose the `to` and `fro` functions, and use
+equational reasoning to combine the inverses.
+\begin{code}
+≃-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)
+    ; fro = λ y → fro A≃B (fro B≃C y)
+    ; invˡ = λ x →
+        begin
+          fro A≃B (fro B≃C (to B≃C (to A≃B x)))
+        ≡⟨ cong (fro A≃B) (invˡ B≃C (to A≃B x)) ⟩
+          fro A≃B (to A≃B x)
+        ≡⟨ invˡ A≃B x ⟩
+          x
+        ∎ 
+    ; invʳ = λ y →
+        begin
+          to B≃C (to A≃B (fro A≃B (fro B≃C y)))
+        ≡⟨ cong (to B≃C) (invʳ A≃B (fro B≃C y)) ⟩
+          to B≃C (fro B≃C y)
+        ≡⟨ invʳ B≃C y ⟩
+          y
+        ∎
+     }
+\end{code}
+
+We will make good use of isomorphisms in what follows to demonstrate
+that operations on types such as product and sum satisfy properties
+akin to associativity, commutativity, and distributivity.
+
+
+## Tabular reasoning for isomorphism
+
+It is straightforward to support a variant of tabular reasoning for
+isomorphism.  We essentially copy the previous definition for
+equivalence.  We omit the form that corresponds to `_≡⟨⟩_`, since
+trivial isomorphisms arise far less often than trivial equivalences.
+
+\begin{code}
+module ≃-Reasoning where
+
+  infix  1 ≃-begin_
+  infixr 2 _≃⟨_⟩_
+  infix  3 _≃-∎
+
+  ≃-begin_ : ∀ {A B : Set} → A ≃ B → A ≃ B
+  ≃-begin A≃B = A≃B
+
+  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set} → A ≃ B → B ≃ C → A ≃ C
+  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C
+
+  _≃-∎ : ∀ (A : Set) → A ≃ A
+  A ≃-∎ = ≃-refl
+
+open ≃-Reasoning
+\end{code}
+
+
+## Embedding
+
+We will also need the notion of *embedding*, which is a weakening
+of isomorphism.  While an isomorphism shows that two types are
+in one-to-one correspondence, and embedding shows that the first
+type is, in a sense, included in the second; or, equivalently,
+that there is a many-to-one correspondence between the second
+type and the first.
+
+Here is the formal definition of embedding.
+\begin{code}
+record _≲_ (A B : Set) : Set where
+  field
+    to : A → B
+    fro : B → A
+    invˡ : ∀ (x : A) → fro (to x) ≡ x
+open _≲_
+\end{code}
+It is the same as an isomorphism, save that it lacks the `invʳ` field.
+Hence, we know that `fro` is left inverse to `to`, but not that it is
+a right inverse.
+
+Embedding is reflexive and transitive.  The proofs are cut down
+versions of the similar proofs for isomorphism, simply dropping the
+right inverses.
+\begin{code}
+≲-refl : ∀ {A : Set} → A ≲ A
+≲-refl =
+  record
+    { to = λ x → x
+    ; fro = λ y → y
+    ; invˡ = λ x → refl
+    } 
+
+≲-tran : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
+≲-tran A≲B B≲C =
+  record
+    { to = λ x → to B≲C (to A≲B x)
+    ; fro = λ y → fro A≲B (fro B≲C y)
+    ; invˡ = λ x →
+        begin
+          fro A≲B (fro B≲C (to B≲C (to A≲B x)))
+        ≡⟨ cong (fro A≲B) (invˡ B≲C (to A≲B x)) ⟩
+          fro A≲B (to A≲B x)
+        ≡⟨ invˡ A≲B x ⟩
+          x
+        ∎ 
+     }
+\end{code}
+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.
+\begin{code}
+≲-antisym : ∀ {A B : Set} → (A≲B : A ≲ B) → (B≲A : B ≲ A) →
+  (to A≲B ≡ fro B≲A) → (fro A≲B ≡ to B≲A) → A ≃ B
+≲-antisym A≲B B≲A to≡fro fro≡to =
+  record
+    { to   = to A≲B
+    ; fro  = fro A≲B
+    ; invˡ = invˡ A≲B
+    ; invʳ = λ y →
+        begin
+          to A≲B (fro A≲B y)
+        ≡⟨ cong (\w → to A≲B (w y)) fro≡to ⟩
+          to A≲B (to B≲A y)
+        ≡⟨ cong (\w → w (to B≲A y)) to≡fro ⟩
+          fro B≲A (to B≲A y)
+        ≡⟨ invˡ B≲A y ⟩
+          y
+        ∎
+    }
+\end{code}
+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 `fro` components from the two embeddings to obtain
+the right inverse of the isomorphism.
+
+
+

src/Logic.lagda

@@ -26,206 +26,13 @@ logic.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
+open import Isomorphism using (_≃_; ≃-sym; _≲_)
+open Isomorphism.≃-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
-
-As a prelude, we begin by introducing the notion of isomorphism.
-In set theory, two sets are isomorphism if they are in 1-to-1 correspondence.
-Here is the formal definition of isomorphism.
-\begin{code}
-record _≃_ (A B : Set) : Set where
-  field
-    to : A → B
-    fro : B → A
-    invˡ : ∀ (x : A) → fro (to x) ≡ x
-    invʳ : ∀ (y : B) → to (fro y) ≡ y
-open _≃_
-\end{code}
-Let's unpack the definition. An isomorphism between sets `A` and `B` consists
-of four things:
-+ A function `to` from `A` to `B`,
-+ A function `fro` from `B` back to `A`,
-+ Evidence `invˡ` asserting that `to` followed by `from` is the identity,
-+ Evidence `invʳ` asserting that `from` followed by `to` is the identity.
-The declaration `open _≃_` makes avaialable the names `to`, `fro`,
-`invˡ`, and `invʳ`, otherwise we would need to write `_≃_.to` and so on.
-
-The above is our first example of a record declaration. It is equivalent
-to a corresponding inductive data declaration.
-\begin{code}
-data _≃′_ : Set → Set → Set where
-  mk-≃′ : ∀ {A B : Set} →
-         ∀ (to : A → B) →
-         ∀ (fro : B → A) → 
-         ∀ (invˡ : (∀ (x : A) → fro (to x) ≡ x)) →
-         ∀ (invʳ : (∀ (y : B) → to (fro y) ≡ y)) →
-         A ≃′ B
-
-to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
-to′ (mk-≃′ f g gfx≡x fgy≡y) = f
-
-fro′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
-fro′ (mk-≃′ f g gfx≡x fgy≡y) = g
-
-invˡ′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → fro′ A≃B (to′ A≃B x) ≡ x)
-invˡ′ (mk-≃′ f g gfx≡x fgy≡y) = gfx≡x
-
-invʳ′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (fro′ A≃B y) ≡ y)
-invʳ′ (mk-≃′ f g gfx≡x fgy≡y) = fgy≡y
-\end{code}
-We construct values of the record type with the syntax:
-
-    record
-      { to = f
-      ; fro = g
-      ; invˡ = gfx≡x
-      ; invʳ = fgy≡y
-      }
-
-which corresponds to using the constructor of the corresponding
-inductive type:
-
-    mk-≃′ f g gfx≡x fgy≡y
-
-where `f`, `g`, `gfx≡x`, and `fgy≡y` are values of suitable types.
-      
-Isomorphism is an equivalence, meaning that it is reflexive, symmetric,
-and transitive.  To show isomorphism is reflexive, we take both `to`
-and `fro` to be the identity function.
-\begin{code}
-≃-refl : ∀ {A : Set} → A ≃ A
-≃-refl =
-  record
-    { to = λ x → x
-    ; fro = λ y → y
-    ; invˡ = λ x → refl
-    ; invʳ = λ y → refl
-    } 
-\end{code}
-To show isomorphism is symmetric, we simply swap the roles of `to`
-and `fro`, and `invˡ` and `invʳ`.
-\begin{code}
-≃-sym : ∀ {A B : Set} → A ≃ B → B ≃ A
-≃-sym A≃B =
-  record
-    { to = fro A≃B
-    ; fro = to A≃B
-    ; invˡ = invʳ A≃B
-    ; invʳ = invˡ A≃B
-    }
-\end{code}
-To show isomorphism is transitive, we compose the `to` and `fro` functions, and use
-equational reasoning to combine the inverses.
-\begin{code}
-≃-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)
-    ; fro = λ y → fro A≃B (fro B≃C y)
-    ; invˡ = λ x →
-        begin
-          fro A≃B (fro B≃C (to B≃C (to A≃B x)))
-        ≡⟨ cong (fro A≃B) (invˡ B≃C (to A≃B x)) ⟩
-          fro A≃B (to A≃B x)
-        ≡⟨ invˡ A≃B x ⟩
-          x
-        ∎ 
-    ; invʳ = λ y →
-        begin
-          to B≃C (to A≃B (fro A≃B (fro B≃C y)))
-        ≡⟨ cong (to B≃C) (invʳ A≃B (fro B≃C y)) ⟩
-          to B≃C (fro B≃C y)
-        ≡⟨ invʳ B≃C y ⟩
-          y
-        ∎
-     }
-\end{code}
-
-We will make good use of isomorphisms in what follows to demonstrate
-that operations on types such as product and sum satisfy properties
-akin to associativity, commutativity, and distributivity.
-
-## Embedding
-
-We will also need the notion of *embedding*, which is a weakening
-of isomorphism.  While an isomorphism shows that two types are
-in one-to-one correspondence, and embedding shows that the first
-type is, in a sense, included in the second; or, equivalently,
-that there is a many-to-one correspondence between the second
-type and the first.
-
-Here is the formal definition of embedding.
-\begin{code}
-record _≲_ (A B : Set) : Set where
-  field
-    to : A → B
-    fro : B → A
-    invˡ : ∀ (x : A) → fro (to x) ≡ x
-open _≲_
-\end{code}
-It is the same as an isomorphism, save that it lacks the `invʳ` field.
-Hence, we know that `fro` is left inverse to `to`, but not that it is
-a right inverse.
-
-Embedding is reflexive and transitive.  The proofs are cut down
-versions of the similar proofs for isomorphism, simply dropping the
-right inverses.
-\begin{code}
-≲-refl : ∀ {A : Set} → A ≲ A
-≲-refl =
-  record
-    { to = λ x → x
-    ; fro = λ y → y
-    ; invˡ = λ x → refl
-    } 
-
-≲-tran : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
-≲-tran A≲B B≲C =
-  record
-    { to = λ x → to B≲C (to A≲B x)
-    ; fro = λ y → fro A≲B (fro B≲C y)
-    ; invˡ = λ x →
-        begin
-          fro A≲B (fro B≲C (to B≲C (to A≲B x)))
-        ≡⟨ cong (fro A≲B) (invˡ B≲C (to A≲B x)) ⟩
-          fro A≲B (to A≲B x)
-        ≡⟨ invˡ A≲B x ⟩
-          x
-        ∎ 
-     }
-\end{code}
-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.
-\begin{code}
-≲-antisym : ∀ {A B : Set} → (A≲B : A ≲ B) → (B≲A : B ≲ A) →
-  (to A≲B ≡ fro B≲A) → (fro A≲B ≡ to B≲A) → A ≃ B
-≲-antisym A≲B B≲A to≡fro fro≡to =
-  record
-    { to   = to A≲B
-    ; fro  = fro A≲B
-    ; invˡ = invˡ A≲B
-    ; invʳ = λ y →
-        begin
-          to A≲B (fro A≲B y)
-        ≡⟨ cong (\w → to A≲B (w y)) fro≡to ⟩
-          to A≲B (to B≲A y)
-        ≡⟨ cong (\w → w (to B≲A y)) to≡fro ⟩
-          fro B≲A (to B≲A y)
-        ≡⟨ invˡ B≲A y ⟩
-          y
-        ∎
-    }
-\end{code}
-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 `fro` components from the two embeddings to obtain
-the right inverse of the isomorphism.
-
 
 ## Conjunction is product
 
@@ -455,7 +262,14 @@ identity, commutativity of product, and symmetry and transitivity of
 isomorphism.
 \begin{code}
 ⊤-identityʳ : ∀ {A : Set} → A ≃ (A × ⊤)
-⊤-identityʳ = ≃-trans (≃-sym ⊤-identityˡ) ×-comm
+⊤-identityʳ {A} =
+  ≃-begin
+    A
+  ≃⟨ ≃-sym ⊤-identityˡ ⟩
+    ⊤ × A
+  ≃⟨ ×-comm {⊤} {A} ⟩
+    A × ⊤
+  ≃-∎
 \end{code}
 
 [TODO: We could introduce a notation similar to that for reasoning on ≡.]
@@ -681,7 +495,14 @@ identity, commutativity of sum, and symmetry and transitivity of
 isomorphism.
 \begin{code}
 ⊥-identityʳ : ∀ {A : Set} → A ≃ (A ⊎ ⊥)
-⊥-identityʳ = ≃-trans (≃-sym ⊥-identityˡ) ⊎-comm
+⊥-identityʳ {A} =
+  ≃-begin
+    A
+  ≃⟨ sym ⊥-identityˡ ⟩
+    ⊤ × A
+  ≃⟨ ⊎-comm ⟩
+    A × ⊤
+  ≃-∎
 \end{code}