updates

2024-07-16 17:44:26 -04:00 · 2024-07-16 17:44:26 -04:00 · 730eeffd75
commit 730eeffd75
parent 00f02ba1ca
5 changed files with 141 additions and 19 deletions
--- a/4
+++ b/4
@ -12,13 +12,15 @@ build-to-html:
 		--allow-unsolved-metas \
 		--html-highlight=auto \
 		--no-load-primitives \
+		--rewriting \
 		|| true
 	# fd --no-ignore "html$$" $(GENDIR) -x rm

 .PHONY: html/src/generated/Progress.md

 html/src/generated/Progress.md:
-	nu scripts/build-table
+	# nu scripts/build-table
+	touch $@

 html/book/Progress.html: html/src/generated/Progress.md
 	pandoc \
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@ -9,6 +9,7 @@
 - [Chapter 3](./generated/HottBook.Chapter3.md)
 - [Chapter 4](./generated/HottBook.Chapter4.md)
 - [Chapter 5](./generated/HottBook.Chapter5.md)
+- [Chapter 6](./generated/HottBook.Chapter6.md)

 # HoTT Book (Cubical formulation)

--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@ -125,7 +125,7 @@ example3∙1∙6 {A} Bset f g p q =
 ### Definition 3.1.7

 ```
-is-1-type : (A : Set) → Set
+is-1-type : (A : Set l) → Set l
 is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
 ```

--- a/src/HottBook/Chapter4.lagda.md
+++ b/src/HottBook/Chapter4.lagda.md
@ -1,3 +1,6 @@
+<details>
+  <summary>Imports</summary>
+
 ```
 module HottBook.Chapter4 where

@ -13,6 +16,8 @@ private
    l : Level
 ```

+</details>
+
 # Chapter 4 Equivalences

 ```
@ -121,7 +126,7 @@ lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {!   !}) , {!   !}
 There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition.

 ```
-theorem4∙1∙3 : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
+-- theorem4∙1∙3 : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
 -- theorem4∙1∙3 {l} = goal
  -- where
  --   goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
@ -230,14 +235,14 @@ lemma4∙2∙9 f q = ({!   !} , {!   !}) , ({!   !} , {!   !})
 module definition4∙2∙10 where
  open definition4∙2∙7

-  lcoh : ∀ {A} {B} → (f : A → B) → linv f → rinv f → Set
+  -- lcoh : ∀ {A} {B} → (f : A → B) → linv f → rinv f → Set
  -- lcoh f (g , η) (g , ε) = ?
 ```

 ### Theorem 4.2.13

 ```
-theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)
+-- theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)
 ```

 ## 4.3 Bi-invertible maps
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@ -11,7 +11,7 @@ open import HottBook.CoreUtil

 private
  variable
-    l : Level
+    l l2 : Level
 ```

 </details>
@ -94,18 +94,20 @@ lemma6∙3∙2 {A = A} {B = B} {f = f} {g = g} p = apd q seg
 ## 6.4 Circles and sphere

 ```
-postulate
-  S¹ : Set
-  base : S¹
-  loop : base ≡ base
+module S¹ where
+  postulate
+    S¹ : Set
+    base : S¹
+    loop : base ≡ base

-  rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
-  rec-S¹-base : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → rec-S¹ {P = P} b l base ≡ b
-  {-# REWRITE rec-S¹-base #-}
-  rec-S¹-loop : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (rec-S¹ b l) loop ≡ l
+    rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
+    rec-S¹-base : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → rec-S¹ {P = P} b l base ≡ b
+    {-# REWRITE rec-S¹-base #-}
+    rec-S¹-loop : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (rec-S¹ b l) loop ≡ l

-  -- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
-  -- {-# REWRITE rec-S¹-loop #-}
+    -- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
+    -- {-# REWRITE rec-S¹-loop #-}
+open S¹ hiding (base)
 ```

 ### Lemma 6.4.1
@ -114,6 +116,8 @@ postulate
 lemma6∙4∙1 : loop ≢ refl
 lemma6∙4∙1 loop≡refl = goal3
  where
+    open S¹
+
    f : ∀ {l} {A : Set l} {x : A} {p : x ≡ x} → S¹ → A
    f {A = A} {x = x} {p = p} = rec-S¹ {P = λ _ → A} x p

@ -144,8 +148,118 @@ lemma6∙4∙2 = f , g
  where
    open axiom2∙9∙3

-    f = rec-S¹ loop {!   !}
+    f = rec-S¹ loop goal
+      where
+        goal : loop ≡[ (λ x → x ≡ x) , loop ] loop
+        goal2 : sym loop ∙ loop ∙ loop ≡ loop
+        goal = lemma2∙11∙2.iii {a = S¹.base} loop loop ∙ goal2
+        goal3 : sym loop ∙ loop ≡ refl
+        goal4 : refl ∙ loop ≡ loop
+        goal5 : sym loop ∙ loop ∙ loop ≡ (sym loop ∙ loop) ∙ loop
+        goal2 = goal5 ∙ ap (λ c → c ∙ loop) goal3 ∙ goal4
+        goal3 = lemma2∙1∙4.ii1 loop
+        goal4 = sym (lemma2∙1∙4.i2 loop)
+        goal5 = lemma2∙1∙4.iv (sym loop) loop loop

    g : f ≡ (λ x → refl) → ⊥
-    g p = {!   !}
-```
+    g p = lemma6∙4∙1 goal
+      where
+        goal : loop ≡ refl
+        goal = ap (λ s → s S¹.base) p
+```
+
+### Corollary 6.4.3
+
+```
+-- corollary6∙4∙3 : (l : Level) → ¬ (is-1-type (Set l))
+-- corollary6∙4∙3 l p = {!   !}
+--   where
+--     open lemma2∙4∙12
+
+--     Circle : Set l
+--     Circle = Lift S¹
+
+--     self : Set (lsuc l)
+--     self = Circle ≡ Circle
+
+--     self-equiv : Set l
+--     self-equiv = Circle ≃ Circle
+
+--     goal1 : ¬ isSet self-equiv
+
+--     goal2 : ¬ isProp (id-equiv Circle ≡ id-equiv Circle)
+--     goal1 p = goal2 λ p' q' → p (id-equiv Circle) (id-equiv Circle) p' q'
+
+--     postulate
+--       equivalence-isProp : isProp self-equiv
+
+--     goal3 : ¬ isProp (id {A = Circle} ≡ id)
+--     goal4 : (id {A = Circle} ≡ id) ≡ (id-equiv Circle ≡ id-equiv Circle)
+
+--     A : Set l
+--     goal : ⊥
+```
+
+### Lemma 6.4.4
+
+```
+lemma6∙4∙4 : {A B : Set} 
+  → (f : A → B)
+  → {x y : A} {p q : x ≡ y}
+  → (r : p ≡ q)
+  → ap f p ≡ ap f q
+lemma6∙4∙4 f refl = refl
+
+ap² = lemma6∙4∙4
+```
+
+### Lemma 6.4.5
+
+```
+lemma6∙4∙5 : {A : Set l}
+  → (P : A → Set l2) 
+  → {x y : A} {p q : x ≡ y}
+  → (r : p ≡ q)
+  → (u : P x)
+  → transport P p u ≡ transport P q u
+lemma6∙4∙5 P refl u = refl
+
+transport² = lemma6∙4∙5
+```
+
+### Lemma 6.4.6
+
+```
+dep-2-path : {l l2 : Level} {A : Set l} {x y : A}
+  → (P : A → Set l2)
+  → {p q : x ≡ y}
+  → (r : p ≡ q)
+  → {u : P x} → {v : P y}
+  → (h : u ≡[ P , p ] v)
+  → (k : u ≡[ P , q ] v)
+  → Set l2
+dep-2-path P r {u = u} h k = h ≡ transport² P r u ∙ k
+
+syntax dep-2-path P r h k = h ≡²[ P , r ] k
+```
+
+```
+lemma6∙4∙6 : {A : Set} {P : A → Set} {x y : A} {p q : x ≡ y}
+  → (f : (x : A) → P x)
+  → (r : p ≡ q)
+  → apd f p ≡²[ P , r ] apd f q
+lemma6∙4∙6 {p = p} f refl = lemma2∙1∙4.i2 (apd f p)
+```
+
+### Sphere
+
+```
+module S² where
+  postulate
+    S² : Set
+    base : S²
+    surf : refl {x = base} ≡ refl
+open S² hiding (base)
+```
+
+## 6.5 Suspensions