From c16fcb22177b99645f097c630898cce60cd61338 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 14 Jul 2024 17:59:07 -0400 Subject: [PATCH] wip --- .vscode/settings.json | 2 +- src/HottBook/Chapter1.lagda.md | 3 +- src/HottBook/Chapter2.lagda.md | 20 ++++-- src/HottBook/Chapter3.lagda.md | 63 ++++++++++++++---- src/HottBook/Chapter6.lagda.md | 113 +++++++++++++++++++++++---------- 5 files changed, 146 insertions(+), 55 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 0e67ce1..e8abc14 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -3,7 +3,7 @@ "gitdoc.enabled": false, "gitdoc.autoCommitDelay": 300000, "gitdoc.commitMessageFormat": "'auto gitdoc commit'", - "agdaMode.connection.commandLineOptions": "--rewriting", + "agdaMode.connection.commandLineOptions": "--rewriting --without-K", "search.exclude": { "src/CubicalHott/**": true } diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 7b87a40..1447719 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -66,7 +66,7 @@ record Σ {l₁ l₂} (A : Set l₁) (B : A → Set l₂) : Set (l₁ ⊔ l₂) field fst : A snd : B fst -open Σ +open Σ public {-# BUILTIN SIGMA Σ #-} syntax Σ A (λ x → B) = Σ[ x ∈ A ] B @@ -145,6 +145,7 @@ infix 3 ¬_ infix 4 _≡_ data _≡_ {A : Set l} : (a b : A) → Set l where instance refl : {x : A} → x ≡ x +{-# BUILTIN EQUALITY _≡_ #-} {-# BUILTIN REWRITE _≡_ #-} ``` diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 821c90a..92cb64f 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -486,7 +486,7 @@ module lemma2∙4∙12 where ### Definition 2.6.1 ``` -definition2∙6∙1 : {A B : Set} {x y : A × B} +definition2∙6∙1 : {A B : Set l} {x y : A × B} → (p : x ≡ y) → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p @@ -496,11 +496,11 @@ definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p ``` module theorem2∙6∙2 where - pair-≡ : {A B : Set} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y + pair-≡ : {A B : Set l} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y pair-≡ (refl , refl) = refl - theorem2∙6∙2 : {A B : Set} {x y : A × B} - → isequiv (definition2∙6∙1 {A} {B} {x} {y}) + theorem2∙6∙2 : {A B : Set l} {x y : A × B} + → isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y}) theorem2∙6∙2 {A} {B} {x} {y} = qinv-to-isequiv (mkQinv pair-≡ backward forward) where backward : (definition2∙6∙1 ∘ pair-≡) ∼ id @@ -508,6 +508,9 @@ module theorem2∙6∙2 where forward : (pair-≡ ∘ definition2∙6∙1) ∼ id forward refl = refl + + pair-≃ : {A B : Set l} {x y : A × B} → (x ≡ y) ≃ ((fst x ≡ fst y) × (snd x ≡ snd y)) + pair-≃ = definition2∙6∙1 , theorem2∙6∙2 open theorem2∙6∙2 using (pair-≡) ``` @@ -808,7 +811,12 @@ module lemma2∙11∙2 where → (p : x1 ≡ x2) → (q : x1 ≡ x1) → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p - iii {l} {A} {a} {x1} {x2} refl refl = refl + iii refl q = + let + a = i1 q + b = i2 q + in b ∙ ap (refl ∙_) a + where open lemma2∙1∙4 ``` ### Theorem 2.11.3 @@ -1013,4 +1021,4 @@ theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward ba backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f backward f = funext λ x → refl where open axiom2∙9∙3 -``` \ No newline at end of file +``` \ No newline at end of file diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 96a8725..1532194 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -35,6 +35,11 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q ``` 𝟙-is-Set : isSet 𝟙 𝟙-is-Set tt tt refl refl = refl + +𝟙-isProp : isProp 𝟙 +𝟙-isProp x y = + let (_ , equiv) = theorem2∙8∙1 x y in + isequiv.g equiv tt ``` ### Example 3.1.3 @@ -48,17 +53,55 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q ``` ℕ-is-Set : isSet ℕ -ℕ-is-Set zero zero refl refl = refl -ℕ-is-Set (suc x) (suc y) refl refl = refl +ℕ-is-Set x y p q = wtf4 + where + open theorem2∙13∙1 + open axiom2∙10∙3 + open isequiv + + cp = encode x y p + cq = encode x y q + + wtf : (x y : ℕ) → (p q : code x y) → p ≡ q + wtf zero zero p q = 𝟙-isProp p q + wtf (suc x) (suc y) p q = wtf x y p q + + wtf2 : (x y : ℕ) → (p q : code x y) → (p ≡ q) → (decode x y p) ≡ (decode x y q) + wtf2 x y p q r = ap (decode x y) r + + wtf3 : {x y : ℕ} → (p : x ≡ y) → (p ≡ decode x y (encode x y p)) + wtf3 {x} {y} p = sym (theorem2∙13∙1 x y .snd .h-id p) + + wtf4 : p ≡ q + wtf4 = (wtf3 p) ∙ wtf2 x y cp cq (wtf x y cp cq) ∙ sym (wtf3 q) ``` ### 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 = refl +×-Set : {A B : Set l} → isSet A → isSet B → isSet (A × B) +×-Set {A = A} {B = B} A-set B-set (xa , xb) (ya , yb) p q = goal + where + open theorem2∙6∙2 + open axiom2∙10∙3 + + p' : (xa ≡ ya) × (xb ≡ yb) + p' = definition2∙6∙1 p + + q' : (xa ≡ ya) × (xb ≡ yb) + q' = definition2∙6∙1 q + + lol : {A B : Set l} {x y : A × B} → (x ≡ y) ≡ ((fst x ≡ fst y) × (snd x ≡ snd y)) + lol = ua pair-≃ + + convert : (p : (xa , xb) ≡ (ya , yb)) → (xa ≡ ya) × (xb ≡ yb) + convert p = definition2∙6∙1 p + + goal : p ≡ q -- (p : (xa, xb)≡(ya, yb)) (q : (xa, xb)≡(ya, yb)) + -- (p': xa≡ya × xb≡yb) + + goal2 = p' ≡ q' + goal = {! ap (λ z → ?) goal2 !} ``` ### Example 3.1.6 @@ -262,12 +305,6 @@ lemma3∙3∙2 : {P : Set} → (x0 : P) → P ≃ 𝟙 lemma3∙3∙2 {P} pp x0 = - let - 𝟙-isProp : isProp 𝟙 - 𝟙-isProp x y = - let (_ , equiv) = theorem2∙8∙1 x y in - isequiv.g equiv tt - in lemma3∙3∙3 pp 𝟙-isProp (λ _ → tt) (λ _ → x0) ``` @@ -639,7 +676,7 @@ module lemma3∙11∙9 where forward p = y (sym (aContr a)) where y : (q : a ≡ a) → transport P q p ≡ p - y refl = refl + y q = {! !} backward : (g ∘ f) ∼ id diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index dbdf1b0..71a0011 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -7,6 +7,7 @@ module HottBook.Chapter6 where open import HottBook.Chapter1 open import HottBook.Chapter2 open import HottBook.Chapter3 +open import HottBook.CoreUtil private variable @@ -22,7 +23,7 @@ Using the approach from here: https://github.com/HoTT/HoTT-Agda/blob/master/old/ ## 6.2 Induction principles and dependent paths ``` -dep-path : {A : Set} {x y : A} → (P : A → Set) → (p : x ≡ y) → (u : P x) → (v : P y) → Set +dep-path : {l l2 : Level} {A : Set l} {x y : A} → (P : A → Set l2) → (p : x ≡ y) → (u : P x) → (v : P y) → Set l2 dep-path P p u v = transport P p u ≡ v syntax dep-path P p u v = u ≡[ P , p ] v @@ -39,27 +40,28 @@ module Interval where I : Set I = #I - 0I : I + 0I 1I : I 0I = #0 - - 1I : I 1I = #1 postulate seg : 0I ≡ 1I - postulate - rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B - - rec-Interval-1 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ b₀ - rec-Interval-2 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 1I ≡ b₁ - - {-# REWRITE rec-Interval-1 #-} - {-# REWRITE rec-Interval-2 #-} + rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B + rec-Interval b₀ b₁ s #0 = b₀ + rec-Interval b₀ b₁ s #1 = b₁ postulate rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s {-# REWRITE rec-Interval-3 #-} + + rec-Interval-d : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → (x : I) → B x + rec-Interval-d b₀ b₁ s #0 = b₀ + rec-Interval-d b₀ b₁ s #1 = b₁ + + postulate + rec-Interval-d-3 : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → apd (rec-Interval-d {B} b₀ b₁ s) seg ≡ s + {-# REWRITE rec-Interval-d-3 #-} open Interval public ``` @@ -69,9 +71,18 @@ open Interval public lemma6∙3∙1 : isContr I lemma6∙3∙1 = 1I , f where + goal : (sym seg) ≡[ (λ z → 1I ≡ z) , seg ] refl + f : (x : I) → 1I ≡ x - f #0 = sym seg - f #1 = refl + f = rec-Interval-d (sym seg) refl goal + + goal2 : transport (λ z → 1I ≡ z) seg (sym seg) ≡ refl + goal = goal2 + + goal3 : (sym seg) ∙ seg ≡ refl + goal2 = lemma2∙11∙2.i seg (sym seg) ∙ goal3 + + goal3 = lemma2∙1∙4.ii1 seg ``` ### Lemma 6.3.2 @@ -103,34 +114,68 @@ base = #base postulate loop : base ≡ base -S¹-rec : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x) -S¹-rec b l #base = b +rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x) +rec-S¹ b l #base = b postulate - S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (S¹-rec b l) loop ≡ l - -{-# REWRITE S¹-rec-loop #-} + 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 +{-# REWRITE rec-S¹-loop #-} ``` ### Lemma 6.4.1 ``` --- lemma6∙4∙1 : loop ≢ refl --- lemma6∙4∙1 loop≡refl = --- {! !} --- where --- f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A) --- f {A = A} {x = x} {p = p} s = --- let p' = transportconst A loop x --- in (S¹-rec x (p' ∙ p)) s --- -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p --- -- f-loop {x = x} = S¹-rec-loop x ? +lemma6∙4∙1 : loop ≢ refl +lemma6∙4∙1 loop≡refl = goal3 + where + -- goal : (s : S¹) (p : s ≡ s) → p ≡ refl + -- goal s p = z1 ∙ z2 ∙ z3 + -- where + -- f : {A : Set} {x : A} {p : x ≡ x} → S¹ → A + -- f {x = x} {p = p} = rec-S¹ x p --- goal : ⊥ + -- z1 : p ≡ apd f loop + -- z1 = refl --- goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A --- goal = example3∙1∙9 (goal2 {! !} {! !} {! !}) + -- z2 : apd f loop ≡ apd f refl + -- z2 = ap (apd f) loop≡refl --- -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl --- goal2 A a p x y r s = {! !} + -- z3 : apd f refl ≡ refl + -- z3 = refl + + goal2 : ∀ {l} {A : Set l} → isSet A + goal2 x .x refl refl = refl + + goal3 : ⊥ + goal3 = example3∙1∙9 (goal2 {A = Set}) + + -- where + -- f : {l : Level} {A : Set l} {x : A} {p : x ≡ x} → (S¹ → A) + -- f {A = A} {x = x} {p = p} s = + -- let p' = transportconst A loop x + -- in (rec-S¹ x (p' ∙ p)) s + -- -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p + -- -- f-loop {x = x} = S¹-rec-loop x ? + + -- goal : ⊥ + + -- goal2 : ∀ {l} → (A : Set l) (a : A) (p : a ≡ a) → isSet A + -- goal = example3∙1∙9 (goal2 Set 𝟙 refl) + + -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl + -- goal2 {l} A a p x y r s = {! !} + -- where + -- f' = f {A = A} {x = a} {p = p} + -- test = apd f' loop ∙ sym (apd f' loop) + + -- z1 : p ≡ apd f' loop + -- z1 = {! !} + + -- z2 : apd f' loop ≡ apd f' refl + -- z2 = {! !} + + -- z3 : apd f' refl ≡ refl + -- z3 = refl + + -- wtf = let wtf = z1 ∙ z2 ∙ z3 in {! !} ``` \ No newline at end of file