update script

2024-07-10 23:06:20 -05:00 · 2024-07-10 23:06:20 -05:00 · b5e43eeb22
commit b5e43eeb22
parent 27524b9250
9 changed files with 151 additions and 50 deletions
--- a/10
+++ b/10
@ -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
--- a/html/ProgressHeader.html
+++ b/html/ProgressHeader.html
@ -0,0 +1,24 @@
+<!DOCTYPE html>
+
+<style>
+  @font-face {
+    font-family: Inter;
+    font-weight: normal;
+    src: url(https://mzhang.io/fonts/Inter-Regular.ttf) format(truetype);
+  }
+  @font-face {
+    font-family: Inter;
+    font-weight: bold;
+    src: url(https://mzhang.io/fonts/Inter-Bold.ttf) format(truetype);
+  }
+  body { font-family: "Inter", sans-serif; }
+  .cell {
+    display: flex;
+    min-height: 48px;
+    align-items: center;
+    justify-content: center;
+    aspect-ratio: 1;
+  }
+</style>
+
+<h1>HoTT Book Progress</h1>
--- 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}}
+  [[original pdf](https://arxiv.org/pdf/1611.02108)]
--- 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" }

-  $"<div style=\"
-      display: flex;
-      align-items: center;
-      justify-content: center;
-      aspect-ratio: 1;
-      min-height: 80px;
+  $"<div class=\"cell\" style=\"
      background-color: ($color);
      color: ($textColor);
    \">
@ -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] }
--- 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)
--- 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
 ```
--- a/src/HottBook/Chapter2Lemma231.lagda.md
+++ 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)
--- a/src/HottBook/Chapter2Util.agda
+++ 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)
--- 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

 ```