From 0a5abb61e40f1235bc875e388645072debbd0923 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 29 Jun 2024 13:25:34 -0500 Subject: [PATCH] a --- .vscode/settings.json | 2 +- src/HottBook/Chapter1.lagda.md | 22 +++-- src/HottBook/Chapter2.lagda.md | 45 ++++++---- src/HottBook/Chapter2Exercises.lagda.md | 13 ++- src/HottBook/Chapter3.lagda.md | 110 +++++++++++++++--------- src/HottBook/CoreUtil.agda | 7 ++ 6 files changed, 122 insertions(+), 77 deletions(-) create mode 100644 src/HottBook/CoreUtil.agda diff --git a/.vscode/settings.json b/.vscode/settings.json index 96ece24..6dabf9e 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -5,6 +5,6 @@ "gitdoc.commitMessageFormat": "'auto gitdoc commit'", "agdaMode.connection.commandLineOptions": "", "search.exclude": { - "src/HottBook/**": true + "src/CubicalHott/**": true } } diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 768f557..e5ab39c 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -5,7 +5,11 @@ module HottBook.Chapter1 where open import Agda.Primitive public -open import Agda.Primitive.Cubical public +open import HottBook.CoreUtil + +private + variable + l : Level ``` @@ -21,7 +25,7 @@ open import Agda.Primitive.Cubical public ## 1.4 Dependent function types (Π-types) ``` -id : {l : Level} {A : Set l} → A → A +id : {A : Set l} → A → A id x = x ``` @@ -94,10 +98,10 @@ rec-+ C f g (inr x) = g x ``` ``` -data ⊥ {l : Level} : Set l where +data ⊥ : Set where -rec-⊥ : {l : Level} → {C : Set l} → (x : ⊥ {l}) → C -rec-⊥ {C} () +rec-⊥ : {C : Set l} → (x : ⊥) → C +rec-⊥ () ``` ## 1.8 The type of booleans @@ -131,22 +135,22 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n) ``` infix 3 ¬_ -¬_ : ∀ {l : Level} (A : Set l) → Set l -¬_ {l} A = A → ⊥ {l} +¬_ : (A : Set l) → Set l +¬_ A = A → ⊥ ``` ## 1.12 Identity types ``` infix 4 _≡_ -data _≡_ {l} {A : Set l} : (a b : A) → Set l where +data _≡_ {A : Set l} : (a b : A) → Set l where instance refl : {x : A} → x ≡ x ``` ### 1.12.3 Disequality ``` -_≢_ : {A : Set} (x y : A) → Set +_≢_ : {A : Set l} (x y : A) → Set l _≢_ x y = (p : x ≡ y) → ⊥ ``` diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 35e6bbc..84c351f 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -5,9 +5,12 @@ module HottBook.Chapter2 where open import Agda.Primitive.Cubical hiding (i1) -open import HottBook.Chapter1 hiding (i1) +open import HottBook.Chapter1 open import HottBook.Chapter2Lemma221 public -open import HottBook.Util + +private + variable + l : Level ``` @@ -632,7 +635,7 @@ postulate ### Lemma 2.9.2 ``` -happly : {A B : Set} +happly : {A B : Set l} → {f g : A → B} → (p : f ≡ g) → (x : A) @@ -644,7 +647,7 @@ happly {A} {B} {f} {g} p x = ap (λ h → h x) p ``` postulate - funext : {l : Level} {A B : Set l} + funext : {A B : Set l} → {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g @@ -707,10 +710,11 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where ### Lemma 2.10.1 ``` -idtoeqv : {l : Level} {A B : Set l} - → (A ≡ B) - → (A ≃ B) -idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A +idtoeqv : {A B : Set l} → (A ≡ B) → (A ≃ B) +idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-homotopy) + where + id-homotopy : (id ∘ id) ∼ id + id-homotopy x = refl ``` ### Axiom 2.10.3 (Univalence) @@ -726,7 +730,7 @@ module axiom2∙10∙3 where backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p -- backward p = {! !} - ua-eqv : {l : Level} {A : Set l} {B : Set l} → (A ≃ B) ≃ (A ≡ B) + ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B) ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward) open axiom2∙10∙3 hiding (forward; backward) @@ -847,10 +851,12 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q = ### Theorem 2.12.5 ``` -module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where +module theorem2∙12∙5 {A B : Set l} (a₀ : A) where + open import HottBook.CoreUtil using (Lift) + code : A + B → Set l code (inl a) = a₀ ≡ a - code (inr b) = ⊥ + code (inr b) = Lift ⊥ encode : (x : A + B) → (p : inl a₀ ≡ x) → code x encode x p = transport code p refl @@ -877,15 +883,16 @@ module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where ### Remark 2.12.6 ``` -remark2∙12∙6 : true ≢ false -remark2∙12∙6 p = genBot tt - where - Bmap : 𝟚 → Set - Bmap true = 𝟙 - Bmap false = ⊥ +module remark2∙12∙6 where + true≢false : true ≢ false + true≢false p = genBot tt + where + Bmap : 𝟚 → Set + Bmap true = 𝟙 + Bmap false = ⊥ - genBot : 𝟙 → ⊥ - genBot = transport Bmap p + genBot : 𝟙 → ⊥ + genBot = transport Bmap p ``` ## 2.13 Natural numbers diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index a8bf905..7f7ae65 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -225,21 +225,18 @@ exercise2∙13 = f , equiv let p1 = ap h' p in let p2 = trans p1 (h-id false) in let p3 = trans (sym (h-id true)) p2 in - remark2∙12∙6 p3 - - ⊥-elim : {l : Level} {A : Set l} → ⊥ {l} → A - ⊥-elim () + remark2∙12∙6.true≢false p3 opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b opposite-prop {a} {b} p with f' (neg a) | inspect f' (neg a) - opposite-prop {true} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q))) + opposite-prop {true} {true} p | true | ingraph q = rec-⊥ (f-codomain-is-2 (trans p (sym q))) opposite-prop {true} {true} p | false | _ = refl opposite-prop {true} {false} p | true | _ = refl - opposite-prop {true} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q))) - opposite-prop {false} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p))) + opposite-prop {true} {false} p | false | ingraph q = rec-⊥ (f-codomain-is-2 (trans p (sym q))) + opposite-prop {false} {true} p | true | ingraph q = rec-⊥ (f-codomain-is-2 (trans q (sym p))) opposite-prop {false} {true} p | false | ingraph q = refl opposite-prop {false} {false} p | true | ingraph q = refl - opposite-prop {false} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p))) + opposite-prop {false} {false} p | false | ingraph q = rec-⊥ (f-codomain-is-2 (trans q (sym p))) f-is-id' : (f' true ≡ true) → (b : 𝟚) → f' b ≡ id b f-is-id' p true = p diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 36f88bd..1cfc2e5 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -10,7 +10,12 @@ open import HottBook.Chapter1Util open import HottBook.Chapter2 open import HottBook.Chapter3Definition331 public open import HottBook.Chapter3Lemma333 public +open import HottBook.CoreUtil open import HottBook.Util + +private + variable + l : Level ``` @@ -20,7 +25,7 @@ open import HottBook.Util ### Definition 3.1.1 ``` -isSet : {l : Level} (A : Set l) → Set l +isSet : (A : Set l) → Set l isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q ``` @@ -34,7 +39,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q ### Example 3.1.3 ``` -⊥-is-Set : ∀ {l} → isSet (⊥ {l}) +⊥-is-Set : isSet ⊥ ⊥-is-Set () () p q ``` @@ -125,56 +130,81 @@ lemma3∙1∙8 {A} A-set x y p q r s = TODO: Study this more ``` -postulate - theorem3∙2∙2 : {l : Level} → ((A : Set l) → ¬ ¬ A → A) → ⊥ {l} --- theorem3∙2∙2 f = let wtf = f 𝟚 in {! !} --- where --- open axiom2∙10∙3 +theorem3∙2∙2 : ((A : Set l) → ¬ ¬ A → A) → ⊥ +theorem3∙2∙2 double-neg = conclusion + where + open axiom2∙10∙3 --- p : 𝟚 ≡ 𝟚 --- p = ua neg-equiv + bool = Lift 𝟚 --- wtf : ¬ ¬ 𝟚 → 𝟚 --- wtf = f 𝟚 + negl : bool → bool + negl (lift true) = lift false + negl (lift false) = lift true --- wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚 --- wtf2 = apd f p + negl-homotopy : (negl ∘ negl) ∼ id + negl-homotopy (lift true) = refl + negl-homotopy (lift false) = refl --- wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u --- wtf3 u = happly wtf2 u + e : bool ≃ bool + e = negl , qinv-to-isequiv (mkQinv negl negl-homotopy negl-homotopy) --- wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u)) --- wtf4 u = --- let --- wtf5 : --- let A = λ A → ¬ ¬ A in --- let B = id in --- transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x)) --- wtf5 = equation2∙9∙4 (f 𝟚) p --- in --- happly wtf5 u + p : bool ≡ bool + p = ua e --- wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v --- wtf6 u v = funext (λ x → rec-⊥ (u x)) + fbool : ¬ ¬ bool → bool + fbool = double-neg bool --- wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u --- wtf7 u = {! !} + apdfp : transport (λ A → ¬ ¬ A → A) p fbool ≡ fbool + apdfp = apd double-neg p --- wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u --- wtf8 u = {! sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u + u : ¬ ¬ bool + u = λ p → p (lift true) --- wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u --- wtf9 = {! !} + foranyu : transport (λ A → ¬ ¬ A → A) p fbool u ≡ fbool u + foranyu = happly apdfp u --- wtf10 : (x : 𝟚) → ¬ (neg x ≡ x) --- wtf10 true p = remark2∙12∙6 (sym p) --- wtf10 false p = remark2∙12∙6 p + what : transport (λ A → ¬ (¬ A) → A) p fbool u ≡ transport (λ X → X) p (fbool (transport (λ X → ¬ (¬ X)) (sym p) u)) + what = + let + x = equation2∙9∙4 {A = λ X → ¬ ¬ X} {B = λ X → X} fbool p + in ap (λ f → f u) x --- wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u)) --- wtf11 u = wtf10 (f 𝟚 u) + allsame : (u v : ¬ ¬ bool) → (x : ¬ bool) → u x ≡ v x + allsame u v x = rec-⊥ (u x) --- wtf12 : (u : ¬ ¬ 𝟚) → ⊥ --- wtf12 u = wtf11 u (wtf9 u) + postulate + allsamef : (u v : ¬ ¬ bool) → u ≡ v + + all-dn-u-same : transport (λ A → ¬ ¬ A) (sym p) u ≡ u + all-dn-u-same = allsamef (transport (λ A → ¬ ¬ A) (sym p) u) u + + nextStep : transport (λ A → A) p (fbool u) ≡ fbool u + nextStep = + let x = ap (λ x → transport id p (fbool x)) all-dn-u-same in + let y = what ∙ x in + sym y ∙ foranyu + + huhh : (Σ.fst e) (fbool u) ≡ fbool u + huhh = + let + equiv1 = ap ua (axiom2∙10∙3.forward e) + + x : {A B : Set l} → (e : A ≃ B) → (a : A) → transport id (ua e) a ≡ Σ.fst e a + x e a = + {! axiom2∙10∙3.forward ? !} + in + sym (x e (fbool u)) ∙ nextStep + + finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x) + finalStep (lift true) p = + let wtf = ap (λ f → Lift.lower f) p in + remark2∙12∙6.true≢false (sym wtf) + finalStep (lift false) p = + let wtf = ap (λ f → Lift.lower f) p in + remark2∙12∙6.true≢false wtf + + conclusion : ⊥ + conclusion = finalStep (fbool u) huhh ``` ### Corollary 3.2.7 diff --git a/src/HottBook/CoreUtil.agda b/src/HottBook/CoreUtil.agda new file mode 100644 index 0000000..eac6abc --- /dev/null +++ b/src/HottBook/CoreUtil.agda @@ -0,0 +1,7 @@ +module HottBook.CoreUtil where + +open import Agda.Primitive + +record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where + constructor lift + field lower : A