chapter 3

html/book.toml

@@ -10,6 +10,9 @@ macros = "./macros.txt"
 
 # [preprocessor.pagetoc]
 
+[preprocessor.chapter-zero]
+levels = [0]
+
 [output.html]
 additional-js = [
     # "theme/pagetoc.js"

html/src/SUMMARY.md

@@ -1,5 +1,6 @@
 # Summary
 
+- [Front](./front.md)
 - [Chapter 1](./generated/HottBook.Chapter1.md)
   - [Exercises](./generated/HottBook.Chapter1Exercises.md)
 - [Chapter 2](./generated/HottBook.Chapter2.md)

html/src/front.md

@@ -0,0 +1,6 @@
+# Homotopy Type Theory
+
+I'm recreating a formalization for the Homotopy Type Theory book as I'm working through it to help me learn.
+
+- [Source](https://git.mzhang.io/school/type-theory)
+

src/HottBook/Chapter1.lagda.md

@@ -86,11 +86,10 @@ rec-+ C f g (inr x) = g x
 ```
 
 ```
-
 data ⊥ : Set where
 
-rec-⊥ : (C : Set) → (x : ⊥) → C
-rec-⊥ C ()
+rec-⊥ : {C : Set} → (x : ⊥) → C
+rec-⊥ {C} ()
 ```
 
 ## 1.8 The type of booleans

src/HottBook/Chapter3.lagda.md

@@ -6,6 +6,8 @@ open import HottBook.Chapter1
 open import HottBook.Chapter1Util
 open import HottBook.Chapter2
 open import HottBook.Chapter2Lemma221
+open import HottBook.Chapter3Definition331
+open import HottBook.Chapter3Lemma333
 open import HottBook.Util
 
 ```
@@ -80,38 +82,51 @@ example3∙1∙9 p = {!   !}
 ### Theorem 3.2.2
 
 ```
--- theorem3∙2∙2 : (A : Set) → (¬ (¬ A) → A) → ⊥
--- theorem3∙2∙2 A p = {!   !}
+theorem3∙2∙2 : ((A : Set) → (¬ (¬ A) → A)) → ⊥
+theorem3∙2∙2 p = {!   !}
+```
+
+### Corollary 3.2.7
+
+```
+corollary3∙2∙7 : ((A : Set) → (A + (¬ A))) → ⊥
+corollary3∙2∙7 g = theorem3∙2∙2 helper
+  where
+    open WithAbstractionUtil
+
+    helper : (A : Set) → (¬ (¬ A)) → A
+    helper A u with g A | inspect g A
+    helper A u | inl a | ingraph q = a
+    helper A u | inr w | ingraph q = rec-⊥ (u w)
 ```
 
 ## 3.3 Mere propositions
 
 ### Definition 3.3.1
 
-```
-isProp : (P : Set) → Set
-isProp P = (x y : P) → x ≡ y
-```
+{{#include HottBook.Chapter3Definition331.md:isProp}}
 
 ### Lemma 3.3.2
 
 ```
--- lemma3∙2∙2 : {P : Set}
---   → isProp P
---   → (x₀ : P)
---   → P ≃ 𝟙
--- lemma3∙2∙2 {P} PisProp x₀ = f , mkIsEquiv g {!  forwards !} g {!   !}
---   where
---     f : P → 𝟙
---     f x = tt
-
---     g : 𝟙 → P
---     g u = x₀
-
---     forwards : f ∘ g ∼ id
---     forwards x = {! refl  !}
+lemma3∙3∙2 : {P : Set}
+  → isProp P
+  → (x0 : P)
+  → P ≃ 𝟙
+lemma3∙3∙2 {P} pp x0 =
+  let
+    𝟙-isProp : isProp 𝟙
+    𝟙-isProp x y = 
+      let (_ , equiv) = theorem2∙8∙1 x y in
+      isequiv.g equiv tt
+  in
+  lemma3∙3∙3 pp 𝟙-isProp (λ _ → tt) (λ _ → x0)
 ```
 
+### Lemma 3.3.3
+
+{{#include HottBook.Chapter3Lemma333.md:lemma333}}
+
 ## 3.4 Classical vs. intuitionistic logic
 
 ### Definition 3.4.3

src/HottBook/Chapter3Definition331.lagda.md

@@ -0,0 +1,15 @@
+```
+module HottBook.Chapter3Definition331 where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+```
+
+[]: ANCHOR: isProp
+
+```
+isProp : (P : Set) → Set
+isProp P = (x y : P) → x ≡ y
+```
+
+[]: ANCHOR_END: isProp

src/HottBook/Chapter3Lemma333.lagda.md

@@ -0,0 +1,28 @@
+```
+module HottBook.Chapter3Lemma333 where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter3Definition331
+```
+
+[]: ANCHOR: lemma333
+
+```
+lemma3∙3∙3 : {P Q : Set}
+  → isProp P
+  → isProp Q
+  → (P → Q)
+  → (Q → P)
+  → P ≃ Q
+lemma3∙3∙3 pp qq f g = f , qinv-to-isequiv (mkQinv g backward forward)
+  where
+    forward : (g ∘ f) ∼ id
+    forward x = pp ((g ∘ f) x) (id x)
+
+    backward : (f ∘ g) ∼ id
+    backward x = qq ((f ∘ g) x) (id x)
+```
+
+[]: ANCHOR_END: lemma333