From e48922ebc5ddfa3a916c1a4647da47409cbef52e Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 2 Jun 2024 17:11:50 -0400
Subject: [PATCH] update front

---
 html/src/front.md                      |  34 ++++-----
 src/CubicalHott/Chapter1.lagda.md      |  39 ++++++++++
 src/CubicalHott/Chapter1Exercises.agda |  31 --------
 src/CubicalHott/Chapter2.lagda.md      |  66 +---------------
 src/CubicalHott/Chapter2Exercises.agda |   8 --
 src/CubicalHott/Chapter3.lagda.md      |  68 +++++++++++++++++
 src/CubicalHott/Chapter6.lagda.md      |  21 ++++++
 src/HottBook/Chapter3.lagda.md         | 100 +++++++++++++------------
 8 files changed, 201 insertions(+), 166 deletions(-)
 delete mode 100644 src/CubicalHott/Chapter1Exercises.agda
 delete mode 100644 src/CubicalHott/Chapter2Exercises.agda
 create mode 100644 src/CubicalHott/Chapter3.lagda.md
 create mode 100644 src/CubicalHott/Chapter6.lagda.md

diff --git a/html/src/front.md b/html/src/front.md
index 885e6bb..a9e8bcb 100644
--- a/html/src/front.md
+++ b/html/src/front.md
@@ -2,23 +2,23 @@
 
 This book tracks my current research goals and progress.
 
-- [Source](https://git.mzhang.io/school/type-theory)
+- [Git repository](https://git.mzhang.io/school/type-theory)
 
-<!-- ```dot process
-digraph {
-  rankdir="BT"
+**Current research:** Formalizing spectral sequences in cubical Agda.
 
-  subgraph cluster_exploration {
-    label = "random cloud of exploration" {
-      mayconcise [label="concise course" URL="https://git.mzhang.io/school/type-theory/raw/branch/master/resources/MayConcise/ConciseRevised.pdf"]
-      hott [label = "hott book" URL="https://hott.github.io/book/hott-ebook.pdf.html"]
-    }
-  }
+## Resources
 
-  subgraph cluster_thesis {
-    label = "thesis" {
-      
-    }
-  }
-}
-``` -->
\ No newline at end of file
+I have scaled down some of these materials to eBook size, for easier reading on mobile phones. The original full PDFs are linked as well.
+
+-
+  Homotopy Type Theory Book
+  [[cached](https://git.mzhang.io/school/type-theory/raw/branch/master/resources/HoTT.pdf)]
+  [[live](https://hott.github.io/book/hott-ebook.pdf.html)]
+-
+  On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, by Floris van Doorn (2018)
+  [[ebook](https://git.mzhang.io/school/type-theory/raw/branch/master/resources/VanDoornDissertation/dissertation.pdf)]
+  [[original](https://florisvandoorn.com/papers/dissertation.pdf)]
+-
+  A Concise Course in Algebraic Topology, by J.P. May (2007)
+  [[ebook](https://git.mzhang.io/school/type-theory/src/branch/master/resources/MayConcise/ConciseRevised.pdf)]
+  [[original](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf)]
diff --git a/src/CubicalHott/Chapter1.lagda.md b/src/CubicalHott/Chapter1.lagda.md
index e69de29..717e257 100644
--- a/src/CubicalHott/Chapter1.lagda.md
+++ b/src/CubicalHott/Chapter1.lagda.md
@@ -0,0 +1,39 @@
+```
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter1 where
+
+-- TODO:
+open import Cubical.Core.Everything public
+```
+
+## 1.7 Coproduct types
+
+```
+data ⊥ {l : Level} : Type l where
+```
+
+## 1.11 Propositions as types
+
+```
+infix 3 ¬_
+¬_ : ∀ {l : Level} (A : Set l) → Set l
+¬_ {l} A = A → ⊥ {l}
+```
+
+## 1.12 Identity types
+
+```
+private
+  to-path : ∀ {l} {A : Type l} → (f : I → A) → Path A (f i0) (f i1)
+  to-path f i = f i
+
+refl : {l : Level} {A : Type l} {x : A} → x ≡ x
+refl {x = x} = to-path (λ i → x)
+```
+
+### 1.12.3 Disequality
+
+```
+_≢_ : {A : Type} (x y : A) → Type
+_≢_ x y = (p : x ≡ y) → ⊥
+```
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter1Exercises.agda b/src/CubicalHott/Chapter1Exercises.agda
deleted file mode 100644
index dc43fa1..0000000
--- a/src/CubicalHott/Chapter1Exercises.agda
+++ /dev/null
@@ -1,31 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module CubicalHott.Chapter1Exercises where
-
-open import Cubical.Core.Everything
-open import Cubical.Core.Primitives public
-open import Data.Empty
-
-refl : {ℓ : Level} {A : Set ℓ} {x : A} → Path A x x
-refl {x = x} = λ i → x
-
--- Exercise 1.1. Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C. Show that we have h ◦ (g ◦ f ) ≡ (h ◦ g) ◦ f .
-infix 10 _∘_
-_∘_ : {A B C : Set} → (g : B → C) → (f : A → B) → A → C
-(g ∘ f) a = g (f a)
-
-exercise-1-1 : {A B C D : Set}
-  → (f : A → B)
-  → (g : B → C)
-  → (h : C → D)
-  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
-exercise-1-1 f g h = refl {x = h ∘ (g ∘ f)}
-
--- TODO: Explain how this works
-
--- Exercise 1.11. Show that for any type A, we have ¬¬¬A → ¬A.
-¬_ : (A : Set) → Set
-¬ A = ⊥
-
-exercise-1-11 : {A : Set} → ¬ (¬ (¬ A)) → ¬ A
-exercise-1-11 ()
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md
index 8f57bb6..49f9fdf 100644
--- a/src/CubicalHott/Chapter2.lagda.md
+++ b/src/CubicalHott/Chapter2.lagda.md
@@ -1,69 +1,9 @@
 ```
 {-# OPTIONS --cubical #-}
 module CubicalHott.Chapter2 where
-open import Cubical.Core.Everything
+
+open import CubicalHott.Chapter1
 ```
 
-# 2.1 Types are higher groupoids
-
-```
-lemma-2-1-2 : {A : Set}
-  → {x y z : A}
-  → x ≡ y
-  → y ≡ z
-  → x ≡ z
-lemma-2-1-2 {A} {x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
-
-_∙_ = lemma-2-1-2
-```
-
-# 2.2 Functions are functors
-
-```
-lemma-2-2-1 : {A B : Set} {x y : A}
-  → (f : A → B)
-  → x ≡ y
-  → f x ≡ f y
-lemma-2-2-1 f p i = f (p i)
-
-ap = lemma-2-2-1
-```
-
-# 2.4 Homotopies and equivalences
-
-```
-definition-2-4-1 : {A : Set} {P : A → Set}
-  → (f g : (x : A) → P x)
-  → Set
-definition-2-4-1 {A} f g = (x : A) → f x ≡ g x
-
-_∼_ = definition-2-4-1
-
-lemma-2-4-2-1 : {A : Set} {P : A → Set}
-  → (f : (x : A) → P x)
-  → f ∼ f
-lemma-2-4-2-1 f x i = f x
-
-lemma-2-4-2-2 : {A : Set} {P : A → Set}
-  → (f g : (x : A) → P x)
-  → (f∼g : f ∼ g)
-  → g ∼ f
-lemma-2-4-2-2 f g f∼g x i = f∼g x (~ i)
-
-lemma-2-4-2-3 : {A : Set} {P : A → Set}
-  → (f g h : (x : A) → P x)
-  → (f∼g : f ∼ g)
-  → (g∼h : g ∼ h)
-  → f ∼ h
-lemma-2-4-2-3 {A} f g h f∼g g∼h x = (f∼g x) ∙ (g∼h x)
--- TODO: Wtf how does this work?
-
-lemma-2-4-3 : {A B : Set}
-  → (f g : A → B)
-  → (H : f ∼ g)
-  → {x y : A}
-  → (p : x ≡ y)
-  → (H x ∙ ap g p) ≡ (ap f p ∙ H y)
-lemma-2-4-3 f g H {x} {y} p i =
-  {!   !}
 ```
+```
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter2Exercises.agda b/src/CubicalHott/Chapter2Exercises.agda
deleted file mode 100644
index 6dc8ca1..0000000
--- a/src/CubicalHott/Chapter2Exercises.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module CubicalHott.Chapter2Exercises where
-
--- Exercise 2.4. Define, by induction on n, a general notion of n-dimensional
--- path in a type A, simultaneously with the type of boundaries for such paths.
-
--- Exercise 2.13. Show that (2 ≃ 2) ≃ 2.
diff --git a/src/CubicalHott/Chapter3.lagda.md b/src/CubicalHott/Chapter3.lagda.md
new file mode 100644
index 0000000..9392dba
--- /dev/null
+++ b/src/CubicalHott/Chapter3.lagda.md
@@ -0,0 +1,68 @@
+```
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter3 where
+
+open import CubicalHott.Chapter1
+```
+
+### Definition 3.1.1
+
+```
+isSet : {l : Level} (A : Type l) → Type l
+isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
+```
+
+### Example 3.1.9
+
+```
+example3∙1∙9 : {l : Level} → ¬ (isSet (Type l))
+example3∙1∙9 p =
+  {!   !}
+  where
+    open import Data.Bool
+    f : Bool → Bool
+    f false = true
+    f true = false
+```
+
+### Definition 3.3.1
+
+```
+isProp : (P : Type) → Type
+isProp P = (x y : P) → x ≡ y
+```
+
+## 3.7 Propositional truncation
+
+```
+module section3∙7 where
+  data ∥_∥ (A : Set) : Set where
+    ∣_∣ : (a : A) → ∥ A ∥
+    witness : (x y : ∥ A ∥) → x ≡ y
+open section3∙7
+```
+
+## 3.8 The axiom of choice
+
+### Equation 3.8.1 (axiom of choice AC)
+
+```
+postulate
+  AC : {X : Type} {A : X → Type} {P : (x : X) → A x → Type}
+    → ((x : X) → ∥ Σ (A x) (λ a → P x a) ∥)
+    → ∥ Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) ∥
+```
+
+### Lemma 3.8.5
+
+```
+```
+
+## 3.9 The principle of unique choice
+
+### Lemma 3.9.1
+
+```
+lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
+lemma3∙9∙1 prop = ∣_∣ , {!   !}
+```
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md
new file mode 100644
index 0000000..0d06155
--- /dev/null
+++ b/src/CubicalHott/Chapter6.lagda.md
@@ -0,0 +1,21 @@
+```
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter6 where
+
+open import CubicalHott.Chapter1
+```
+
+## 6.4 Circles and spheres
+
+```
+data S¹ : Type where
+  base : S¹
+  loop : base ≡ base
+```
+
+### Lemma 6.4.1
+
+```
+lemma6∙4∙1 : loop ≢ refl
+lemma6∙4∙1 p = {!   !}
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index f351988..3a4cf74 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -41,8 +41,44 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.4
 
 ```
--- ℕ-is-Set : isSet ℕ
--- ℕ-is-Set = 
+ℕ-is-Set : isSet ℕ
+ℕ-is-Set zero zero refl refl = refl
+ℕ-is-Set (suc x) (suc y) refl refl = refl
+```
+
+### Example 3.1.5
+
+TODO: DO this without path induction
+
+```
+×-Set : {A B : Set} → isSet A → isSet B → isSet (A × B)
+×-Set {A} {B} A-set B-set (xa , xb) (ya , yb) refl refl =
+  let
+    open theorem2∙6∙2
+
+    -- p-pair = definition2∙6∙1 p
+    -- q-pair = definition2∙6∙1 q
+
+    -- a-eq = A-set xa ya (Σ.fst p-pair) (Σ.fst q-pair)
+    -- b-eq = B-set xb yb (Σ.snd p-pair) (Σ.snd q-pair)
+
+    -- overall = pair-≡ {xa ≡ ya} {xb ≡ yb} {p-pair} {q-pair} (a-eq , b-eq)
+  in refl
+```
+
+### Definition 3.1.7
+
+```
+is-1-type : (A : Set) → Set
+is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
+```
+
+### Lemma 3.1.8
+
+```
+lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
+lemma3∙1∙8 {A} A-set x y p q r s =
+  {!   !}
 ```
 
 ### Example 3.1.9
@@ -176,58 +212,28 @@ lemma3∙3∙2 {P} pp x0 =
 
 ### Definition 3.4.3
 
-#### i. Decidability of types
-
 ```
--- decidable : (A : Set) → Set
--- decidable A = A ⊎ ¬ A
+module definition3∙4∙3 where
+  data decidable (A : Set) : Set where
+    proof : A + (¬ A) → decidable A
+
+  data decidable2 {A : Set} (B : A → Set) : Set where
+    proof : (a : A) → (B a + (¬ (B a))) → decidable2 B
+
+  data decidable-equality (A : Set) : Set where
+    proof : (a b : A) → ((a ≡ b) + (¬ a ≡ b)) → decidable-equality A
 ```
 
-#### ii. Decidability of type families
+## 3.5 Subsets and propositional resizing
 
 ```
--- dep-decidable : {A : Set} → (B : A → Set) → Set
--- dep-decidable {A} B = (a : A) → (B a ⊎ ¬ B a)
-```
-
-#### iii. Decidable equality
 
-```
--- decidable-equality : (A : Set) → Set
--- 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.
+## 3.7 Propositional truncation
 
 ```
--- decidable-equality-is-set : (A : Set) → 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 ?
-```
+module section3∙7 where
+  data ∥_∥ (A : Set) : Set where
+    ∣_∣ : (a : A) → ∥ A ∥
+```
\ No newline at end of file