From 491b1b87b03c4166fab7cb64dac1e36e309982eb Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 5 Aug 2024 11:17:04 -0400 Subject: [PATCH] wip --- src/CubicalHott/Chapter6.lagda.md | 9 ++ src/HottBook/Chapter1.lagda.md | 6 ++ src/HottBook/Chapter3.lagda.md | 8 +- src/HottBook/Chapter6.lagda.md | 132 +++++++++++++++------------ src/HottBook/Chapter6Circle.lagda.md | 6 +- src/HottBook/Chapter7.lagda.md | 88 +++++++++++++----- src/HottBook/Chapter8.lagda.md | 13 +-- 7 files changed, 164 insertions(+), 98 deletions(-) diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md index 38ef916..ea3f2fd 100644 --- a/src/CubicalHott/Chapter6.lagda.md +++ b/src/CubicalHott/Chapter6.lagda.md @@ -83,4 +83,13 @@ lemma6∙4∙2 : Σ ((x : S¹) → x ≡ x) (λ y → y ≢ (λ x → refl)) -- z2 = z base -- z3 = lemma6∙4∙1 z2 -- in z3 +``` + +``` +circle-is-contractible : isContr S¹ +circle-is-contractible = base , f + where + f : (x : S¹) → base ≡ x + f base = refl + f (loop i) j = {! !} ``` \ No newline at end of file diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 623d260..d3c0de8 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -120,6 +120,12 @@ neg true = false neg false = true ``` +``` +if_then_else_ : {A : Set} → 𝟚 → A → A → A +if true then x else y = x +if false then x else y = y +``` + ## 1.9 The natural numbers ``` diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 60b3869..eb68abc 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -39,9 +39,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q 𝟙-is-Set tt tt refl refl = refl 𝟙-isProp : isProp 𝟙 -𝟙-isProp x y = - let (_ , equiv) = theorem2∙8∙1 x y in - isequiv.g equiv tt +𝟙-isProp tt tt = refl ``` ### Example 3.1.3 @@ -374,8 +372,8 @@ module definition3∙4∙3 where data decidable-family {A : Set} (B : A → Set) : Set where proof : (a : A) → (B a + (¬ (B a))) → decidable-family B - data decidable-equality (A : Set) : Set where - proof : ((a b : A) → (a ≡ b) + (¬ a ≡ b)) → decidable-equality A + decidable-equality : (A : Set) → Set + decidable-equality A = (a b : A) → (a ≡ b) + (¬ a ≡ b) ``` ## 3.5 Subsets and propositional resizing diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index f4cc444..d8b59e5 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -83,7 +83,6 @@ module Interval where {-# REWRITE rec-Interval-1I #-} 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-0I : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → rec-Interval-d {B = B} b₀ b₁ s 0I ≡ b₀ @@ -92,7 +91,6 @@ module Interval where {-# REWRITE rec-Interval-d-1I #-} 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 ``` @@ -194,38 +192,19 @@ lemma6∙4∙2 = f , g ### Corollary 6.4.3 ``` -corollary6∙4∙3 : (l : Level) → ¬ (is-1-type (Set l)) -corollary6∙4∙3 l p = {! !} - where - open lemma2∙4∙12 +corollary6∙4∙3 : ¬ (is-1-type Set) +corollary6∙4∙3 = {! !} where + open ≃-Reasoning + open lemma2∙4∙12 + open axiom2∙9∙3 + open axiom2∙10∙3 + open S¹ - Circle : Set l - Circle = Lift S¹ + goal : ¬ is-1-type Set + + goal2 : ¬ isSet (S¹ ≡ S¹) + goal prf = goal2 (prf S¹ 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' - - goal2 = {! !} - - -- postulate - -- equivalence-isProp : isProp self-equiv - - -- goal3 : ¬ isProp (id {A = Circle} ≡ id) - -- goal2 prop = goal3 λ x y → {! !} - - -- goal4 : (id {A = Circle} ≡ id) ≃ (id-equiv Circle ≡ id-equiv Circle) - -- goal4 = f , {! !} - -- where - -- f : (id {A = Circle} ≡ id) → (id-equiv Circle ≡ id-equiv Circle) - -- f p = ap (λ z → z , {! mkIsEquiv id (λ _ → refl) id (λ _ → refl) !}) p ``` ### Lemma 6.4.4 @@ -328,36 +307,71 @@ open Suspension public ``` lemma6∙5∙1 : Susp 𝟚 ≃ S¹ -lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward) - where - open S¹ +lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward) where + open S¹ + open ≡-Reasoning - m : 𝟚 → base ≡ base - m true = refl - m false = loop + m : 𝟚 → base ≡ base + m = λ b → if b then refl else loop - f : Susp 𝟚 → S¹ - f s = rec-Susp base base m s + f : Susp 𝟚 → S¹ + f = rec-Susp base base m + -- f N = base + -- f S = base + -- f (merid b) = if b then refl else loop - g : S¹ → Susp 𝟚 - g s = rec-S¹ N (merid false ∙ sym (merid true)) s - -- g : S¹ → Susp 𝟚 - -- g base = N - -- g loop = (merid false ∙ sym (merid true)) + g : S¹ → Susp 𝟚 + g = rec-S¹ N (merid false ∙ sym (merid true)) + -- g base = N + -- g loop = merid false ∙ sym (merid true) + + forward : (f ∘ g) ∼ id + forward x = rec-S¹ refl {! !} x + + backward : (x : Susp 𝟚) → g (f x) ≡ x + backward x = ind-Susp {P = λ z → g (f z) ≡ z} refl (merid true) goal x where + goal : (a : 𝟚) → transport (λ z → g (f z) ≡ z) (merid a) refl ≡ (merid true) - forward : (f ∘ g) ∼ id - forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl p x - where - p : refl ≡[ (λ x → f (g x) ≡ x) , loop ] refl - p = {! merid true !} - - backward : (g ∘ f) ∼ id - backward x = ind-Susp {P = λ y → g (f y) ≡ y} refl (merid true) goal x - where - goal : (y : 𝟚) → transport (λ z → g (f z) ≡ z) (merid y) refl ≡ merid true + goal2 : (a : 𝟚) → sym (ap g (ap f (merid a))) ∙ refl ∙ merid a ≡ merid true + goal a = {! !} - goal2 : (y : 𝟚) → {! !} ∙ refl ∙ {! !} ≡ merid true - goal y = {! !} + goal3 : (a : 𝟚) → sym (ap g (ap f (merid a))) ∙ merid a ≡ merid true + goal2 a = ap (sym (ap g (ap f (merid a))) ∙_) (sym (lemma2∙1∙4.i2 (merid a))) ∙ goal3 a + + goal3 true = + sym (ap g (ap f (merid true))) ∙ merid true ≡⟨ ap (_∙ merid true) (ap (λ z → sym (ap g z)) (rec-Susp-merid base base m true)) ⟩ + sym (ap g refl) ∙ merid true ≡⟨ sym (lemma2∙1∙4.i2 (merid true)) ⟩ + merid true ∎ + goal3 false = {! !} + +-- lemma6∙5∙1 : Susp 𝟚 ≃ S¹ +-- lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward) +-- where +-- open S¹ + +-- m : 𝟚 → base ≡ base +-- m true = refl +-- m false = loop + +-- f : Susp 𝟚 → S¹ +-- f s = rec-Susp base base m s + +-- g : S¹ → Susp 𝟚 +-- g s = rec-S¹ N (merid false ∙ sym (merid true)) s + +-- forward : (f ∘ g) ∼ id +-- forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl p x +-- where +-- p : refl ≡[ (λ x → f (g x) ≡ x) , loop ] refl +-- p = {! merid true !} + +-- backward : (g ∘ f) ∼ id +-- backward x = ind-Susp {P = λ y → g (f y) ≡ y} refl (merid true) goal x +-- where +-- goal : (y : 𝟚) → transport (λ z → g (f z) ≡ z) (merid y) refl ≡ merid true + +-- goal2 : (y : 𝟚) → {! !} ∙ refl ∙ {! !} ≡ merid true +-- goal y = {! !} ``` ### Definition 6.5.2 @@ -466,4 +480,6 @@ module Pushout where Pushout : {A B C : Set} → (f : C → A) → (g : C → B) → Set syntax Pushout A B C = A ⊔[ C ] B -``` \ No newline at end of file +``` + +## asdf \ No newline at end of file diff --git a/src/HottBook/Chapter6Circle.lagda.md b/src/HottBook/Chapter6Circle.lagda.md index 5e82669..b2e0b52 100644 --- a/src/HottBook/Chapter6Circle.lagda.md +++ b/src/HottBook/Chapter6Circle.lagda.md @@ -25,13 +25,11 @@ module S¹ where 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¹ : {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 #-} + 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 open S¹ hiding (base) public ``` diff --git a/src/HottBook/Chapter7.lagda.md b/src/HottBook/Chapter7.lagda.md index 0b5ed89..9dcbb13 100644 --- a/src/HottBook/Chapter7.lagda.md +++ b/src/HottBook/Chapter7.lagda.md @@ -41,6 +41,20 @@ theorem7∙1∙4 {X} {Y} f negtwo q = f (fst q) , λ y → {! !} theorem7∙1∙4 {X} {Y} f (suc n) q = {! !} ``` +### Corollary 7.1.5 + +``` +corollary7∙1∙5 : {X Y : Set} → X ≃ Y → (n : ℕ') → is n type X → is n type Y +corollary7∙1∙5 eqv n X-ntype = theorem7∙1∙4 (fst eqv) n X-ntype +``` + +## 7.2 Uniqueness of identity proofs and Hedberg’s theorem + +### Theorem 7.2.1 + +``` +``` + ### Theorem 7.2.2 ``` @@ -63,27 +77,27 @@ module lemma2∙9∙6 where Prop : {l : Level} → Set (lsuc l) Prop {l} = Σ (Set l) isProp -theorem7∙2∙2 : {l : Level} {X : Set l} → {R : X → X → Prop {l = l}} - → (ρ : (x : X) → R x x) - → (f : (x y : X) → R x y → x ≡ y) → isSet X -theorem7∙2∙2 {X} {R} ρ f = {! !} - where - variable - x : X - p : x ≡ x - r : R x x +-- theorem7∙2∙2 : {l : Level} {X : Set l} → {R : X → X → Prop {l = l}} +-- → (ρ : (x : X) → R x x) +-- → (f : (x y : X) → R x y → x ≡ y) → isSet X +-- theorem7∙2∙2 {X} {R} ρ f = {! !} +-- where +-- variable +-- x : X +-- p : x ≡ x +-- r : R x x - apdfp : transport (λ x → x ≡ x) p (f x x (ρ x)) ≡ f x x (ρ x) - apdfp {p = p} = apd (λ x → f x x (ρ x)) p +-- apdfp : transport (λ x → x ≡ x) p (f x x (ρ x)) ≡ f x x (ρ x) +-- apdfp {p = p} = apd (λ x → f x x (ρ x)) p - step2 : {x : X} {p : x ≡ x} - → (r : R x x) - → transport (λ z → z ≡ z) p (f x x r) ≡ f x x (transport (λ z → R z z) p r) - step2 {x} {p} r = - let - f' = f x x - helper = lemma2∙9∙6.stmt {A = λ z → R z z} p f' f' - in (fst helper) refl (ρ x) +-- step2 : {x : X} {p : x ≡ x} +-- → (r : R x x) +-- → transport (λ z → z ≡ z) p (f x x r) ≡ f x x (transport (λ z → R z z) p r) +-- step2 {x} {p} r = +-- let +-- f' = f x x +-- helper = lemma2∙9∙6.stmt {A = λ z → R z z} p f' f' +-- in (fst helper) refl (ρ x) ``` ### Lemma 7.2.4 @@ -107,14 +121,14 @@ theorem7∙2∙3 x y u = ``` theorem7∙2∙5 : {X : Set} → definition3∙4∙3.decidable-equality X → isSet X -theorem7∙2∙5 {X} (definition3∙4∙3.proof f) x y p q with prf ← f x y in eq = helper prf eq - where - helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q - helper (inl z) eq = theorem7∙2∙3 x y (λ n → n p) x y p q - helper (inr g) eq = rec-⊥ (g p) +-- theorem7∙2∙5 {X} d x y p q with prf ← d x y in eq = helper prf eq +-- where +-- helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q +-- helper (inl z) eq = theorem7∙2∙3 x y (λ n → n p) x y p q +-- helper (inr g) eq = rec-⊥ (g p) hedberg : {X : Set} → definition3∙4∙3.decidable-equality X → isSet X -hedberg {X} (definition3∙4∙3.proof d) x y p q = {! !} +hedberg {X} d x y p q = {! !} where open ≡-Reasoning -- d : (a b : X) → (a ≡ b) + (¬ a ≡ b) @@ -130,6 +144,7 @@ hedberg {X} (definition3∙4∙3.proof d) x y p q = {! !} helper (inr x) = rec-⊥ (x p) r-constant : (x y : X) → (p q : x ≡ y) → r x y p ≡ r x y q + r-constant x y p q = {! !} s : (x y : X) → x ≡ y → x ≡ y s x y p = sym (r x x refl) ∙ r x y p @@ -152,4 +167,27 @@ hedberg {X} (definition3∙4∙3.proof d) x y p q = {! !} -- helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q -- helper (inl z) eq = {! !} -- helper (inr g) eq = rec-⊥ (g p) +``` + +### Theorem 7.2.6 + +``` +open theorem2∙13∙1 +theorem7∙2∙6 : definition3∙4∙3.decidable-equality ℕ +theorem7∙2∙6 zero zero = inl refl +theorem7∙2∙6 zero (suc y) = inr (encode zero (suc y)) +theorem7∙2∙6 (suc x) zero = inr (encode (suc x) zero) +theorem7∙2∙6 (suc x) (suc y) with IH ← theorem7∙2∙6 x y = helper IH where + helper : (x ≡ y) + (x ≡ y → ⊥) → (suc x ≡ suc y) + (suc x ≡ suc y → ⊥) + helper (inl p) = inl (ap suc p) + helper (inr f) = inr λ p → f (decode x y (encode (suc x) (suc y) p)) +``` + +### Theorem 7.2.8 + +## 7.3 Truncations + +### Lemma 7.3.1 + +``` ``` \ No newline at end of file diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md index 4e11f07..4b6bc00 100644 --- a/src/HottBook/Chapter8.lagda.md +++ b/src/HottBook/Chapter8.lagda.md @@ -18,7 +18,7 @@ open import HottBook.CoreUtil ### Definition 8.0.1 ``` -π : (n : ℕ) → (A : Set) → (a : A) → Set +-- π : (n : ℕ) → (A : Set) → (a : A) → Set -- π n A a = ∥ ? ∥₀ ``` @@ -75,8 +75,9 @@ module definition8∙1∙1 where backward (lift (negsuc zero)) = refl backward (lift (negsuc (suc x))) = refl - code : {l : Level} → S¹ → Set l - code = rec-S¹ Int (ua zsuc-equiv) + code : {l : Level} → Lift S¹ → Set l + -- code = rec-S¹ Int (ua zsuc-equiv) + code (lift s) = rec-S¹ Int (ua zsuc-equiv) s ``` ### Lemma 8.1.2 @@ -91,10 +92,10 @@ module lemma8∙1∙2 where lifted-loop : {l : Level} → lift base ≡ lift base lifted-loop {l} = ap (lift {l = l}) loop - i : {l : Level} → (x : Int {l}) → (transport code loop x) ≡ int-suc x + i : {l : Level} → (x : Int {l}) → (transport code lifted-loop x) ≡ int-suc x i x = begin - (transport code loop x) ≡⟨ lemma2∙3∙10 id code {! lifted-loop !} x ⟩ - (transport id (ap code loop) x) ≡⟨ {! !} ⟩ + (transport code lifted-loop x) ≡⟨ lemma2∙3∙10 id code {! lifted-loop !} x ⟩ + (transport id (ap code lifted-loop) x) ≡⟨ {! !} ⟩ -- (transport id (ua int-suc) x) ≡⟨ {! !} ⟩ int-suc x ∎