diff --git a/Makefile b/Makefile
index 75bc087..97f8808 100644
--- a/Makefile
+++ b/Makefile
@@ -17,6 +17,16 @@ build-to-html:
build-book: build-to-html
mdbook build html
+ pandoc \
+ -f markdown-markdown_in_html_blocks+raw_html \
+ -t html \
+ -i html/src/generated/Progress.md \
+ > html/book/Progress.html
+ mkdir -p html/book/progress
+ cat \
+ html/ProgressHeader.html \
+ html/book/Progress.html \
+ > html/book/progress/index.html
refresh-book: build-to-html
mdbook serve html
diff --git a/html/ProgressHeader.html b/html/ProgressHeader.html
new file mode 100644
index 0000000..19bc558
--- /dev/null
+++ b/html/ProgressHeader.html
@@ -0,0 +1,24 @@
+
+
+
+
+
HoTT Book Progress
\ No newline at end of file
diff --git a/html/src/front.md b/html/src/front.md
index f7ceba4..32daf15 100644
--- a/html/src/front.md
+++ b/html/src/front.md
@@ -3,6 +3,7 @@
This book tracks my current research goals and progress.
- [Git repository](https://git.mzhang.io/school/type-theory)
+- [HoTT Book Formalization Progress](https://mzhang.io/research/progress/)
**Current research:** Formalizing spectral sequences in cubical Agda.
@@ -24,8 +25,4 @@ I have scaled down some of these materials to eBook size, for easier reading on
-
Cubical Type Theory: a constructive interpretation of the univalence axiom (CCHM) (2015)
[[ebook-sized pdf](https://git.mzhang.io/school/type-theory/raw/branch/master/resources/CCHM/main.pdf)]
- [[original pdf](https://arxiv.org/pdf/1611.02108)]
-
-## HottBook Progress:
-
-{{#include generated/Progress.md}}
\ No newline at end of file
+ [[original pdf](https://arxiv.org/pdf/1611.02108)]
\ No newline at end of file
diff --git a/scripts/build-table b/scripts/build-table
index 12d6da5..a8c74d3 100755
--- a/scripts/build-table
+++ b/scripts/build-table
@@ -8,7 +8,7 @@ let chapters = {
let gradients = [
[0, [90, 0, 0]],
- [0.5, [90, 90, 0]],
+ [0.65, [180, 180, 0]],
[1, [0, 90, 0]],
]
@@ -34,12 +34,7 @@ let viz = { |k, n|
let color = if $n == 0 { "gray" } else { do $interpColor ($k / $n) }
let textColor = if $k == $n { "gold" } else { "white" }
- $"
@@ -74,7 +69,6 @@ $chapters
| sort-by Ch
| tee { save -f html/src/generated/Progress.md }
-
# open breakdown.json
# | transpose
# | each {|row| [$row.column0, $row.column1.ratioCompleted] }
\ No newline at end of file
diff --git a/src/HottBook/Chapter1Util.agda b/src/HottBook/Chapter1Util.agda
index d6dbb9c..399c53c 100644
--- a/src/HottBook/Chapter1Util.agda
+++ b/src/HottBook/Chapter1Util.agda
@@ -2,7 +2,7 @@ module HottBook.Chapter1Util where
open import Agda.Primitive
open import HottBook.Chapter1
-open import HottBook.Chapter2
+open import HottBook.Chapter2Lemma231
open import HottBook.Util
Σ-≡ : {l₁ l₂ : Level} {A : Set l₁} {B : A → Set l₂}
@@ -10,10 +10,3 @@ open import HottBook.Util
→ Σ (a₁ ≡ a₂) (λ p → transport B p b₁ ≡ b₂)
→ p₁ ≡ p₂
Σ-≡ {l₁} {l₂} {A} {B} {p₁ @ (a₁ , b₁)} {p₂ @ (a₂ , b₂)} (refl , refl) = refl
-
-neg-homotopy : (neg ∘ neg) ∼ id
-neg-homotopy true = refl
-neg-homotopy false = refl
-
-neg-equiv : 𝟚 ≃ 𝟚
-neg-equiv = neg , qinv-to-isequiv (mkQinv neg neg-homotopy neg-homotopy)
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index b2f2914..b767921 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -6,7 +6,9 @@ module HottBook.Chapter2 where
open import Agda.Primitive.Cubical hiding (i1)
open import HottBook.Chapter1
+open import HottBook.Chapter1Util
open import HottBook.Chapter2Lemma221 public
+open import HottBook.Chapter2Lemma231 public
private
variable
@@ -85,31 +87,25 @@ module lemma2∙1∙4 {l : Level} {A : Set l} where
This comes first, since it is needed to define Theorem 2.1.6.
```
-record pointed (l : Level) : Set (lsuc l) where
- eta-equality
- constructor mkPointed
- field
- A : Set l
- a : A
+pointed : {l : Level} → Set (lsuc l)
+pointed {l} = Σ (Set l) (λ A → A)
```
### Definition 2.1.8 (loop space)
```
-Ω : {l : Level} → pointed l → pointed l
-Ω (mkPointed A a) = mkPointed (a ≡ a) refl
+Ω : {l : Level} → pointed {l} → pointed {l}
+Ω (A , a) = (a ≡ a) , refl
```
### Theorem 2.1.6 (Eckmann-Hilton)
```
module theorem2∙1∙6 where
- open pointed
-
- Ω² : {l : Level} → pointed l → pointed l
+ Ω² : {l : Level} → pointed {l} → pointed {l}
Ω² p = Ω (Ω p)
- -- compose : {l : Level} → (p : pointed l) → Ω² p
+ -- compose : {l : Level} {p : pointed {l}} → (Ω² p) × (Ω² p) → Ω² p
-- compose a b = ?
```
@@ -142,15 +138,7 @@ module lemma2∙2∙2 {A B C : Set} where
## 2.3 Type families are fibrations
-### Lemma 2.3.1 (Transport)
-
-```
-transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
- → (P : A → Set l₂)
- → (p : x ≡ y)
- → P x → P y
-transport {l₁} {l₂} {A} {x} {y} P refl = id
-```
+{{#include HottBook.Chapter2Lemma231.md:transport}}
### Lemma 2.3.2 (Path lifting property)
@@ -589,7 +577,9 @@ corollary2∙7∙3 z = refl
-- → {x y : A}
-- → (p : x ≡ y)
-- → (u z : Σ (P x) (λ u → Q (x , u)))
--- → transport {! P !} p (u , z) ≡ (transport {! P !} p u , transport {! !} (pair-≡ (p , refl)) z)
+-- → transport (λ x → Σ (Σ (P x) λ u → Q (x , u)) λ _ → Σ (P x) λ u → Q (x , u)) p (u , z)
+-- ≡ ( transport (λ x → Σ (P x) λ u → Q (x , u)) p u
+-- , transport (λ (m , n) → {! Σ (P y) ? !}) (Σ-≡ (p , refl)) z)
```
## 2.8 The unit type
@@ -647,8 +637,8 @@ happly {A} {B} {f} {g} p x = ap (λ h → h x) p
```
postulate
- funext : ∀ {l} {A B : Set l}
- → {f g : A → B}
+ funext : ∀ {l l2} {A : Set l} {B : A → Set l2}
+ → {f g : (x : A) → B x}
→ ((x : A) → f x ≡ g x)
→ f ≡ g
```
diff --git a/src/HottBook/Chapter2Lemma231.lagda.md b/src/HottBook/Chapter2Lemma231.lagda.md
new file mode 100644
index 0000000..3f0e00c
--- /dev/null
+++ b/src/HottBook/Chapter2Lemma231.lagda.md
@@ -0,0 +1,20 @@
+```
+module HottBook.Chapter2Lemma231 where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+```
+
+### Lemma 2.3.1 (Transport)
+
+[//]: <> (ANCHOR: transport)
+
+```
+transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
+ → (P : A → Set l₂)
+ → (p : x ≡ y)
+ → P x → P y
+transport {l₁} {l₂} {A} {x} {y} P refl = id
+```
+
+[//]: <> (ANCHOR_END: transport)
\ No newline at end of file
diff --git a/src/HottBook/Chapter2Util.agda b/src/HottBook/Chapter2Util.agda
new file mode 100644
index 0000000..7043fe2
--- /dev/null
+++ b/src/HottBook/Chapter2Util.agda
@@ -0,0 +1,11 @@
+module HottBook.Chapter2Util where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+
+neg-homotopy : (neg ∘ neg) ∼ id
+neg-homotopy true = refl
+neg-homotopy false = refl
+
+neg-equiv : 𝟚 ≃ 𝟚
+neg-equiv = neg , qinv-to-isequiv (mkQinv neg neg-homotopy neg-homotopy)
\ No newline at end of file
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 24bd5bb..c612f81 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -8,6 +8,7 @@ open import Agda.Primitive
open import HottBook.Chapter1
open import HottBook.Chapter1Util
open import HottBook.Chapter2
+open import HottBook.Chapter2Util
open import HottBook.Chapter3Definition331 public
open import HottBook.Chapter3Lemma333 public
open import HottBook.CoreUtil
@@ -63,7 +64,7 @@ TODO: DO this without path induction
### Example 3.1.6
```
--- example3∙1∙6 : {A : Set} {B : A → Set} → ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
+example3∙1∙6 : {A : Set} {B : A → Set} → ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
-- example3∙1∙6 func f g p q =
-- let
-- wtf : p ≡ funext (λ x → happly p x)
@@ -277,6 +278,23 @@ module definition3∙4∙3 where
```
+## 3.6 The logic of mere propositions
+
+### Example 3.6.1
+
+```
+example3∙6∙1 : {A B : Set} → isProp A → isProp B → isProp (A × B)
+example3∙6∙1 {A} {B} Aprop Bprop =
+ λ (x1 , x2) (y1 , y2) → Σ-≡ (Aprop x1 y1 , transportconst B (Aprop x1 y1) x2 ∙ Bprop x2 y2)
+```
+
+### Example 3.6.2
+
+```
+example3∙6∙2 : {A : Set} {B : A → Set} → ((x : A) → isProp (B x)) → isProp ((x : A) → B x)
+example3∙6∙2 {A} {B} allProps = λ f g → funext λ x → allProps x (f x) (g x)
+```
+
## 3.7 Propositional truncation
```
@@ -301,9 +319,6 @@ open section3∙7 public
lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
where
- thing2 : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ (∣ a ∣) ∣ ≡ ∣ a ∣)
- thing2 = rec-∥ P ∥ prop ∣_∣
-
thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ a)
thing = rec-∥ P ∥ prop id
@@ -321,7 +336,7 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
eqP = prop gx gy
gpx = g-prop gx
in
- {! !}
+ admit
where
postulate
-- TODO: Finish this
@@ -337,6 +352,53 @@ isContr : (A : Set l) → Set l
isContr A = Σ A (λ a → (x : A) → a ≡ x)
```
+### Lemma 3.11.3
+
+```
+module lemma3∙11∙3 where
+ record properties (A : Set l) : Set l where
+ constructor mkProperties
+ field
+ i : isContr A
+ ii : A × isProp A
+ iii : A ≃ 𝟙
+
+ i : {A : Set} → isContr A → properties A
+ i Acontr @ (a , aEq) = mkProperties p1 p2 p3
+ where
+ p1 = Acontr
+ p2 = a , λ x y → sym (aEq x) ∙ aEq y
+
+ forward : ((λ _ → tt) ∘ (λ _ → a)) ∼ id
+ forward tt = refl
+ p3 = (λ _ → tt) , qinv-to-isequiv (mkQinv (λ _ → a) forward aEq)
+
+ ii : {A : Set} → A × isProp A → properties A
+ ii Aprop @ (a , aProp) = mkProperties p1 p2 p3
+ where
+ p1 = a , aProp a
+ p2 = Aprop
+
+ forward : ((λ _ → tt) ∘ (λ _ → a)) ∼ id
+ forward tt = refl
+ p3 = (λ _ → tt) , qinv-to-isequiv (mkQinv (λ _ → a) forward (aProp a))
+
+ iii : {A : Set} → A ≃ 𝟙 → properties A
+ iii Aeqv @ (f , mkIsEquiv g g* h h*) = mkProperties p1 p2 p3
+ where
+ p1 = g tt , λ x → {! ap g ? !}
+ p2 = g tt , λ x y → {! !}
+ p3 = Aeqv
+
+```
+
+### Lemma 3.11.6
+
+```
+lemma3∙11∙6 : {A : Set} {P : A → Set} → ((a : A) → isContr (P a)) → isContr ((x : A) → P x)
+lemma3∙11∙6 {A} {P} allContr = {! !}
+```
+
### Lemma 3.11.8
```