From e39a01960248177ca65f6c3bb2135dd1f9d74f9f Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 31 Jan 2018 12:53:08 -0200 Subject: [PATCH] factored out Isomorphism, Logic broken --- index.md | 10 +- src/Equivalence.lagda | 114 ++++++++++++++++++-- src/Isomorphism.lagda | 242 ++++++++++++++++++++++++++++++++++++++++++ src/Logic.lagda | 215 ++++--------------------------------- 4 files changed, 372 insertions(+), 209 deletions(-) create mode 100644 src/Isomorphism.lagda diff --git a/index.md b/index.md index 8b1f1e99..bd13954d 100644 --- a/index.md +++ b/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 diff --git a/src/Equivalence.lagda b/src/Equivalence.lagda index 2fb64d65..9dd88d46 100644 --- a/src/Equivalence.lagda +++ b/src/Equivalence.lagda @@ -4,6 +4,9 @@ layout : page permalink : /Equivalence --- + + 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 -import would create a conflict. +definition of equivalence. Since we define equivalence here, any such +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 -value is equivalent to itself, and we have no other way of showing values -are equivalent. Here we have quantified over all levels, so that -we can apply equivalence to types belonging to any level. +constructor `refl` provides evidence that `x ≡ x`. Hence, every value +is equivalent to itself, and we have no other way of showing values +are equivalent. We have quantified over all levels, so that we can +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.) diff --git a/src/Isomorphism.lagda b/src/Isomorphism.lagda new file mode 100644 index 00000000..c1cc26ca --- /dev/null +++ b/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. + + + diff --git a/src/Logic.lagda b/src/Logic.lagda index 90c150c1..84b7f5ab 100644 --- a/src/Logic.lagda +++ b/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}