From b5e43eeb22052344c29c253a51aaf488b5501af4 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 10 Jul 2024 23:06:20 -0500 Subject: [PATCH] update script --- Makefile | 10 ++++ html/ProgressHeader.html | 24 +++++++++ html/src/front.md | 7 +-- scripts/build-table | 10 +--- src/HottBook/Chapter1Util.agda | 9 +--- src/HottBook/Chapter2.lagda.md | 38 +++++--------- src/HottBook/Chapter2Lemma231.lagda.md | 20 +++++++ src/HottBook/Chapter2Util.agda | 11 ++++ src/HottBook/Chapter3.lagda.md | 72 ++++++++++++++++++++++++-- 9 files changed, 151 insertions(+), 50 deletions(-) create mode 100644 html/ProgressHeader.html create mode 100644 src/HottBook/Chapter2Lemma231.lagda.md create mode 100644 src/HottBook/Chapter2Util.agda 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 ```