From 085f1462529f6639c21499a4a0fea63f8be3d610 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 2 Oct 2024 01:43:05 -0500 Subject: [PATCH] wip --- src/CubicalHott/Definition8-5-4.agda | 17 +++ src/CubicalHott/Lemma8-5-5.agda | 17 +++ src/CubicalHott/Theorem7-1-11.agda | 40 +++++++ src/CubicalHott/Theorem7-1-4.agda | 45 ++++++++ src/CubicalHott/Theorem8-1.agda | 107 ++++++++++++++----- src/HoTTEST/Agda/Cubical/Exercises8.lagda.md | 8 +- 6 files changed, 203 insertions(+), 31 deletions(-) create mode 100644 src/CubicalHott/Definition8-5-4.agda create mode 100644 src/CubicalHott/Lemma8-5-5.agda create mode 100644 src/CubicalHott/Theorem7-1-11.agda create mode 100644 src/CubicalHott/Theorem7-1-4.agda diff --git a/src/CubicalHott/Definition8-5-4.agda b/src/CubicalHott/Definition8-5-4.agda new file mode 100644 index 0000000..6a8ad22 --- /dev/null +++ b/src/CubicalHott/Definition8-5-4.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --cubical #-} + +module CubicalHott.Definition8-5-4 where + +open import Agda.Primitive +open import Cubical.Foundations.Prelude +open import Cubical.Data.Sigma + +record H-Space (A : Type) : Type where + field + e : A + μ : A → A → A + + left : (a : A) → μ e a ≡ a + right : (a : A) → μ a e ≡ a + +open H-Space public \ No newline at end of file diff --git a/src/CubicalHott/Lemma8-5-5.agda b/src/CubicalHott/Lemma8-5-5.agda new file mode 100644 index 0000000..cb8044a --- /dev/null +++ b/src/CubicalHott/Lemma8-5-5.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --cubical #-} + +module CubicalHott.Lemma8-5-5 where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import CubicalHott.Definition8-5-4 + +lemma : {A : Type} → (H : H-Space A) → (a : A) → isEquiv (λ e → (H-Space.μ H) a e) +lemma {A} H a = isoToIsEquiv (iso f g {! !} {! !}) where + f : A → A + f e = (H-Space.μ H) a e + + g : A → A + + diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda new file mode 100644 index 0000000..992af06 --- /dev/null +++ b/src/CubicalHott/Theorem7-1-11.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --cubical #-} + +module CubicalHott.Theorem7-1-11 where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Core.Glue +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Data.Nat +open import Data.Unit + +lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n) +lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , {! !} where + -- G : A ≡ B + -- G = ua (isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)) + + -- g : PathP (λ i → G i) a b + -- g = {! !} + + -- contr : Acontr ≡ Bcontr + + eqv1 : A ≃ B + eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr) + + T = λ { (i = i0) → A ; (i = i1) → B } + e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B } + + G = primGlue B T e + g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b + + contr : (y : G) → g ≡ y + contr y j = {! !} + + -- unglue i {! !} + -- (glue (λ { (i = i1) → {! !} }) {! !}) + -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b)) +lemma (suc n) x y = {! !} + \ No newline at end of file diff --git a/src/CubicalHott/Theorem7-1-4.agda b/src/CubicalHott/Theorem7-1-4.agda new file mode 100644 index 0000000..d1cff02 --- /dev/null +++ b/src/CubicalHott/Theorem7-1-4.agda @@ -0,0 +1,45 @@ +{-# OPTIONS --cubical #-} + +module CubicalHott.Theorem7-1-4 where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Homotopy.Base +open import Cubical.Data.Nat + +theorem : {X Y : Type} + → (p : X → Y) + → (s : Y → X) + → retract s p + → (n : ℕ) + → isOfHLevel n X + → isOfHLevel n Y +theorem {X} {Y} p s r zero (x0 , xContr) = p x0 , λ y → cong p (xContr (s y)) ∙ r y +theorem {X} {Y} p s r (suc zero) xHlevel a b = + let + step1 = xHlevel (s a) (s b) + step2 = cong p step1 + step3 = (sym (r a)) ∙ step2 ∙ r b + in step3 +theorem {X} {Y} p s r (suc (suc n)) xHlevel a b = + {! !} where + ε : (p ∘ s) ∼ idfun Y + + + -- -- X is h-level (n+2) + -- -- If X is h-level (n+1), then Y is h-level (n+1) + -- theorem f (cong p') z (suc n) xOfHLevel where + -- f : p' a ≡ p' b → a ≡ b + -- f = λ q → sym (r a) ∙ cong p q ∙ r b + + -- z : retract (λ q i → p' (q i)) f + -- z q = + -- f (λ i → p' (q i)) ≡⟨⟩ + -- sym (r a) ∙ cong p (λ i → p' (q i)) ∙ r b ≡⟨ {! !} ⟩ + -- sym (r a) ∙ cong p (λ i → p' (q i)) ∙ r b ≡⟨ {! !} ⟩ + -- q ∎ + + -- xOfHLevel = xHlevel (p' a) (p' b) + diff --git a/src/CubicalHott/Theorem8-1.agda b/src/CubicalHott/Theorem8-1.agda index 285e170..1d80c7c 100644 --- a/src/CubicalHott/Theorem8-1.agda +++ b/src/CubicalHott/Theorem8-1.agda @@ -5,13 +5,17 @@ module CubicalHott.Theorem8-1 where open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Pointed +open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Prelude +open import Cubical.Homotopy.Group.Base open import Cubical.Foundations.Function open import Cubical.Foundations.Univalence open import Cubical.HITs.S1 hiding (encode; decode) +open import Cubical.HITs.SetTruncation open import Cubical.Homotopy.Loopspace open import Cubical.Data.Nat hiding (pred; _+_) renaming (suc to nsuc) -open import Data.Integer +open import Cubical.Data.Int +open import Cubical.Data.Int.Base open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10) @@ -22,17 +26,18 @@ private -- Definition 8.1.1 suc≃ : ℤ ≃ ℤ -suc≃ = isoToEquiv (iso suc pred sec ret) where - sec : section suc pred - sec (+_ zero) = refl - sec +[1+ n ] = refl - sec (-[1+_] zero) = refl - sec (-[1+_] (nsuc n)) = refl - ret : retract suc pred - ret (+_ zero) = refl - ret +[1+ n ] = refl - ret (-[1+_] zero) = refl - ret (-[1+_] (nsuc n)) = refl +suc≃ = isoToEquiv (iso sucℤ predℤ sec ret) where + sec : section sucℤ predℤ + sec (pos zero) = refl + sec (pos (nsuc n)) = refl + sec (negsuc zero) = refl + sec (negsuc (nsuc n)) = refl + + ret : retract sucℤ predℤ + ret (pos zero) = refl + ret (pos (nsuc n)) = refl + ret (negsuc zero) = refl + ret (negsuc (nsuc n)) = refl suc≡ : ℤ ≡ ℤ suc≡ = ua suc≃ @@ -42,37 +47,85 @@ code base = ℤ code (loop i) = suc≡ i loop⁻ : ℤ → base ≡ base -loop⁻ (+_ zero) = refl -loop⁻ +[1+ n ] = loop⁻ (+ n) ∙ loop -loop⁻ (-[1+_] zero) = loop⁻ (+ zero) ∙ (sym loop) -loop⁻ (-[1+_] (nsuc n)) = loop⁻ -[1+ n ] ∙ (sym loop) +loop⁻ (pos zero) = refl +loop⁻ (pos (nsuc n)) = loop⁻ (pos n) ∙ loop +loop⁻ (negsuc zero) = sym loop +loop⁻ (negsuc (nsuc n)) = loop⁻ (negsuc n) ∙ sym loop -- Lemma 8.1.2 -lemma8-1-2a : (x : ℤ) → subst code loop x ≡ suc x +lemma8-1-2a : (x : ℤ) → subst code loop x ≡ sucℤ x lemma8-1-2a x = subst code loop x ≡⟨ lemma2-3-10 (idfun S¹) code loop x ⟩ subst (idfun Type) (cong code loop) x ≡⟨⟩ subst (idfun Type) suc≡ x ≡⟨⟩ - suc x ∎ + sucℤ x ∎ -- Definition 8.1.5 encode : (x : S¹) → base ≡ x → code x -encode s p = subst code p +0 +encode s p = subst code p (pos zero) -- Definition 8.1.6 +lemma1 : (x : ℤ) → loop⁻ (predℤ x) ∙ loop ≡ loop⁻ x +lemma1 (pos zero) = rCancel (sym loop) +lemma1 (pos (nsuc n)) = refl +lemma1 (negsuc zero) = + sym (assoc ? ? ?) + ∙ cong (λ p → sym loop ∙ p) (lCancel ?) + ∙ sym (rUnit (sym loop)) +lemma1 (negsuc (nsuc n)) = {! refl !} + decode : (x : S¹) → code x → base ≡ x decode base c = loop⁻ c -decode (loop i) c j = - let u = λ k → λ where - (i = i0) → {! !} - (i = i1) → loop⁻ c j - (j = i0) → base - (j = i1) → loop (i ∨ ~ k) - in hcomp u {! !} +decode (loop i) c j = path j (unglue (~ i ∨ i) c) {! i !} where + + path : subst (λ x' → code x' → base ≡ x') loop loop⁻ ≡ loop⁻ + path = + subst (λ x' → (code x' → base ≡ x')) loop loop⁻ + ≡⟨ {! !} ⟩ + subst (λ x' → base ≡ x') loop ∘ loop⁻ ∘ subst code (sym loop) + ≡⟨⟩ + (λ p → p ∙ loop) ∘ loop⁻ ∘ subst code (sym loop) + ≡⟨⟩ + (λ p → p ∙ loop) ∘ loop⁻ ∘ predℤ + ≡⟨ {! !} ⟩ + (λ n → loop⁻ (predℤ n) ∙ loop) + ≡⟨ funExt lemma1 ⟩ + loop⁻ + ∎ + -- we are trying to prove that loop⁻ c j ≡ loop⁻ c j + -- but on one side it's refl_base, and on the other, it's loop i + -- let + -- bottomFace = let u = λ j → λ where + -- (i = i0) → {! !} + -- (i = i1) → {! !} + -- in hfill u (inS {! !}) {! j !} + + -- u = λ k → λ where + -- (i = i0) → {! !} + -- (i = i1) → loop⁻ c j + -- (j = i0) → base + -- (j = i1) → loop (i ∨ ~ k) + -- in hcomp u bottomFace + +-- Theorem 8.1.9 + +theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x) +theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) {! !} {! !}) -- Corollary 8.1.10 -corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , +0 \ No newline at end of file +corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , pos zero +corollary8-1-10 = theorem8-1-9 base , refl + +-- Corollary 8.1.11 + +corollary8-1-11 : π 1 (S¹ , base) ≡ ℤ +corollary8-1-11 = + π 1 (S¹ , base) ≡⟨⟩ + ∥ typ (Ω (S¹ , base)) ∥₂ ≡⟨⟩ + ∥ base ≡ base ∥₂ ≡⟨ cong ∥_∥₂ (ua (fst corollary8-1-10)) ⟩ + ∥ ℤ ∥₂ ≡⟨ setTruncIdempotent isSetℤ ⟩ + ℤ ∎ \ No newline at end of file diff --git a/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md b/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md index 4d4a47d..1b4b22b 100644 --- a/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md +++ b/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md @@ -58,7 +58,7 @@ transport computes away at `i = i1`. ```agda fromPathP : {A : I → Type ℓ} {x : A i0} {y : A i1} → PathP A x y → transport (λ i → A i) x ≡ y -fromPathP {A = A} {x = x} p i = {! !} +fromPathP {A = A} {x = x} p i = transp (λ j → A (i ∨ j)) i (p i) ``` ### Exercise 3 (★★★) @@ -87,9 +87,9 @@ toPathP : {A : I → Type ℓ} {x : A i0} {y : A i1} → transport (λ i → A i) x ≡ y → PathP A x y toPathP {A = A} {x = x} p i = hcomp - (λ {j (i = i0) → {!!} ; - j (i = i1) → {!!} }) - {!!} + (λ {j (i = i0) → x ; + j (i = i1) → p i }) + {! !} ``` ### Exercise 4 (★)