added material on isomorphism to Logic

src/Logic.lagda

@@ -12,7 +12,92 @@ function, dependent product, Martin Löf equivalence).
 ## Imports
 
 \begin{code}
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+\end{code}
+
+This chapter introduces the basic concepts of logic, including
+conjunction, disjunction, true, false, implication, negation,
+universal quantification, and existential quantification.
+Each concept of logic is represented by a corresponding standard
+data type.
+
++ *conjunction* is *product*
++ *disjunction* is *sum*
++ *true* is *unit type*
++ *false* is *empty type*
++ *implication* is *function space*
++ *negation* is *function to empty type*
++ *universal quantification* is *dependent function*
++ *existential quantification* is *dependent product*
+
+We also discuss how equality is represented, and the relation
+between *intuitionistic* and *classical* logic.
+
+
+## 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.
+
+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 symmetric, we compose the `to` and `fro` functions, and use
+equational reasoning to combine the inverses.
+\begin{code}
+≃-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
+      ∎ ;
+    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}
 
 ## Conjunction
@@ -38,6 +123,17 @@ infixr 2 _×_
 infixr 4 _,_
 \end{code}
 
+Product is associative and commutative up to isomorphism.
+\begin{code}
+×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C))
+×-assoc =
+  record {
+    to = λ { ((x , y) , z) → (x , (y , z)) };
+    fro = λ { (x , (y , z)) → ((x , y) , z) };
+    invˡ = λ { ((x , y) , z) → refl } ;
+    invʳ = λ { (x , (y , z)) → refl }
+  }
+\end{code}
 
 
 ## Disjunction
@@ -67,6 +163,7 @@ and `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 
 Distribution of `×` over `⊎` is an isomorphism.
 \begin{code}
+{-
 data _≃_ : Set → Set → Set where
   mk-≃ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
           (∀ (x : A) → g (f x) ≡ x) → (∀ (y : B) → f (g y) ≡ y) → A ≃ B
@@ -90,10 +187,12 @@ data _≃_ : Set → Set → Set where
   fg : ∀ {A B C : Set} → (y : (A × C) ⊎ (B × C)) → f (g y) ≡ y
   fg (inj₁ (a , c)) = refl
   fg (inj₂ (b , c)) = refl
+-}
 \end{code}
 
 Distribution of `⊎` over `×` is half an isomorphism.
 \begin{code}
+{-
 data _≲_ : Set → Set → Set where
   mk-≲ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
           (∀ (x : A) → g (f x) ≡ x) → A ≲ B
@@ -115,6 +214,7 @@ data _≲_ : Set → Set → Set where
   gf : ∀ {A B C : Set} → (x : (A × B) ⊎ C) → g (f x) ≡ x
   gf (inj₁ (a , b)) = refl
   gf (inj₂ c) = refl
+-}
 \end{code}
 
 ## True

src/extra/Reasoning.agda

@@ -4,9 +4,10 @@ import Relation.Binary.PropositionalEquality as Eq
 import Relation.Binary.PreorderReasoning as Re
 
 module ReEq = Re (Eq.preorder ℕ)
-open ReEq using (begin_; _∎) renaming (_≈⟨⟩_ to _≡⟨⟩_; _∼⟨_⟩_ to _≡⟨_⟩_)
+open ReEq using (begin_; _∎; _IsRelatedTo_) renaming (_≈⟨⟩_ to _≡⟨⟩_; _∼⟨_⟩_ to _≡⟨_⟩_)
 open Eq using (_≡_; refl; sym; trans)
 
+
 lift : ∀ {m n : ℕ} → m ≡ n → suc m ≡ suc n
 lift refl = refl