From 6d0e500a5945015d4e93fa4f3661d87e4f0b8418 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 18 May 2023 03:28:13 -0500
Subject: [PATCH] updates

---
 src/HottBook/Chapter1.lagda.md | 23 ++++++++++
 src/HottBook/Chapter2.lagda.md | 38 +++++++++++++++-
 src/HottBook/Chapter3.lagda.md | 80 ++++++++++++++++++++++++++++++++++
 3 files changed, 140 insertions(+), 1 deletion(-)
 create mode 100644 src/HottBook/Chapter1.lagda.md
 create mode 100644 src/HottBook/Chapter3.lagda.md

diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
new file mode 100644
index 0000000..2833c08
--- /dev/null
+++ b/src/HottBook/Chapter1.lagda.md
@@ -0,0 +1,23 @@
+```
+module HottBook.Chapter1 where
+
+open import Data.Empty
+open import Data.Sum
+
+Type = Set
+```
+
+## 1.7 Coproduct types
+
+```
+infixl 6 _+_
+_+_ : (A B : Type) → Type
+A + B = A ⊎ B
+```
+
+## 1.11 Propositions as types
+
+```
+¬_ : (A : Type) → Type
+¬ A = A → ⊥
+```
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 68256ee..eeecd0d 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -145,7 +145,7 @@ _∼_ {A} f g = (x : A) → f x ≡ g x
 
 ### Lemma 2.4.2
 
-Homotopy forms an equivalence:
+Homotopy forms an equivalence relation:
 
 ```
 ∼-refl : {A : Type} {P : A → Type} (f : (x : A) → P x) → f ∼ f
@@ -189,6 +189,26 @@ id-qinv = record
   }
 ```
 
+### Definition 2.4.10
+
+```
+linv : {A B : Type} (f : A → B) → Type
+linv {A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g) ∼ id
+
+rinv : {A B : Type} (f : A → B) → Type
+rinv {A} {B} f = Σ[ h ∈ (B → A) ] (h ∘ f) ∼ id
+
+isEquiv : {A B : Type} (f : A → B) → Type
+isEquiv f = linv f × rinv f
+```
+
+### Definition 2.4.11
+
+```
+_≃_ : (A B : Type) → Type
+A ≃ B = Σ[ f ∈ (A → B) ] isEquiv f
+```
+
 ## 2.8 The unit type
 
 ```
@@ -239,3 +259,19 @@ happly f g {x} p =
 postulate
   funext : {A B : Type} → (f g : A → B) → {x : A} → (p : f x ≡ g x) → f ≡ g
 ```
+
+## 2.10 Universes and the univalence axiom
+
+### Lemma 2.10.1
+
+```
+-- idToEquiv : {A B : Type} → (A ≡ B) → A ≃ B
+-- idToEquiv p = ? , ?
+```
+
+### Axiom 2.10.3 (Univalence)
+
+```
+postulate
+  ua : {A B : Type} (eqv : A ≃ B) → (A ≡ B)
+```
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
new file mode 100644
index 0000000..aec74bc
--- /dev/null
+++ b/src/HottBook/Chapter3.lagda.md
@@ -0,0 +1,80 @@
+```
+module HottBook.Chapter3 where
+
+open import Relation.Binary.PropositionalEquality
+open import Data.Sum
+open import Data.Empty
+open import HottBook.Chapter1
+
+```
+
+## 3.1 Sets and n-types
+
+### Definition 3.1.1
+
+```
+isSet : (A : Type) → Type
+isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
+```
+
+## 3.2 Propositions as types?
+
+## 3.4 Classical vs. intuitionistic logic
+
+### Definition 3.4.3
+
+#### i. Decidability of types
+
+```
+decidable : (A : Type) → Type
+decidable A = A ⊎ ¬ A
+```
+
+#### ii. Decidability of type families
+
+```
+dep-decidable : {A : Type} → (B : A → Type) → Type
+dep-decidable {A} B = (a : A) → (B a ⊎ ¬ B a)
+```
+
+#### iii. Decidable equality
+
+```
+decidable-equality : (A : Type) → Type
+decidable-equality A = (a b : A) → (a ≡ b) ⊎ ¬ (a ≡ b)
+```
+
+So I think the interesting property about this is that normally a function f
+would return something of the type a ≡ b, which for any a and b would always
+produce that one path. But there could exist other functions that produce
+different paths, like (g : ... → a ≡ b).
+
+What this (a ≡ b) ⊎ ¬ (a ≡ b) business is saying is: if f couldn't produce a
+path, then **NO** other functions will ever be able to produce paths (along with
+a proof that this is true). This means f is _exclusively_ the deciding factor
+for whether a and b are equal under this type, and it's the only one that mints
+paths for a ≡ b.
+
+---
+
+> 2. In case you are looking for advanced exercises, you can try to prove that
+> any type with decidable equality is a set.
+
+```
+decidable-equality-is-set : (A : Type) → decidable-equality A → isSet A
+decidable-equality-is-set A f x y p q =
+  let
+    res = f x y
+
+    -- We can eliminate the bottom case because if p and q exist, it must be inj₁
+    center : x ≡ y
+    center = [ (λ p′ → p′) , (λ p′ → ⊥-elim (p′ _)) ] (f x y)
+
+    -- What i want is: given any path x ≡ y, prove that it equals this inj₁ (res f x y)
+    guarantee : (p′ : x ≡ y) → center ≡ p′
+    guarantee p′ = J (λ the what → the ≡ p′) ? ?
+
+    info = ?
+  in
+  J (λ the what → p ≡ ?) refl ?
+```