From 4bbcf990d26015280e83b7ac3fd0078fe2c716d8 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 12 Dec 2024 15:14:18 -0600 Subject: [PATCH] =?UTF-8?q?proved:=20f(1)=E2=89=A1id=20in=20EMSpace?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Misc/STLCLogRel.agda | 17 ++++-- src/ThesisWork/EMSpace.agda | 110 +++++++++++++++++++++++++++--------- 2 files changed, 93 insertions(+), 34 deletions(-) diff --git a/src/Misc/STLCLogRel.agda b/src/Misc/STLCLogRel.agda index 99ccfbe..0973d72 100644 --- a/src/Misc/STLCLogRel.agda +++ b/src/Misc/STLCLogRel.agda @@ -152,16 +152,21 @@ postulate part2 : {e : term} → {τ : type} → term-rel τ e → safe e part2 t s with res ← decide-irred {! !} = {! !} -fundamental type-`unit = λ γ x → e-term f where +fundamental type-`unit γ x = e-term f where f : {n : ℕ} (e' : term) → steps n `unit e' → irreducible e' → value-rel unit e' f e' zero i = v-`unit -fundamental type-`true = λ γ x → e-term f where +fundamental type-`true γ x = e-term f where f : {n : ℕ} (e' : term) → steps n `true e' → irreducible e' → value-rel bool e' f e' zero i = v-`true -fundamental type-`false = λ γ x → e-term f where +fundamental type-`false γ x = e-term f where f : {n : ℕ} (e' : term) → steps n `false e' → irreducible e' → value-rel bool e' f e' zero i = v-`false -fundamental (type-`ifthenelse p p₁ p₂) = {! !} +fundamental {τ = τ} (type-`ifthenelse {e = e} {e₁ = e₁} {e₂ = e₂} p p₁ p₂) γ x = e-term (f e) where + f : (e : term) {n : ℕ} (e' : term) → steps n (`if e then e₁ else e₂) e' → irreducible e' → value-rel τ e' + f e e' zero i = ⊥-elim {! e !} + f e e' (suc n x s) i = {! !} fundamental (type-`x p) γ (cons {v = v} γ-good v-value) = e-term (λ e' s i → {! !}) -fundamental (type-`λ p) = λ γ x → {! !} -fundamental (type-∙ p p₁) = {! !} \ No newline at end of file +fundamental (type-`λ p) γ x = e-term (λ e' steps irred → {! v-`λ[_]_ !}) +fundamental {τ = τ} (type-∙ {e₁ = e₁} {e₂ = e₂} p p₁) γ γ-good = e-term f where + f : {n : ℕ} (e' : term) → steps n (e₁ ∙ e₂) e' → irreducible e' → value-rel τ e' + f e' s i = {! !} \ No newline at end of file diff --git a/src/ThesisWork/EMSpace.agda b/src/ThesisWork/EMSpace.agda index 05f4395..955d051 100644 --- a/src/ThesisWork/EMSpace.agda +++ b/src/ThesisWork/EMSpace.agda @@ -7,12 +7,13 @@ open import Cubical.Algebra.Group.Base open import Cubical.Algebra.Monoid open import Cubical.Algebra.Semigroup open import Cubical.Algebra.Group.Morphisms -open import Cubical.Data.Nat +open import Cubical.Data.Nat hiding (_·_) open import Cubical.Foundations.Function open import Cubical.Foundations.HLevels open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence open import Cubical.Foundations.Pointed open import Cubical.Foundations.Prelude open import Cubical.Foundations.Structure @@ -20,19 +21,53 @@ open import Cubical.Homotopy.Loopspace open import Cubical.Homotopy.Group.Base open import Cubical.HITs.SetTruncation as ST hiding (rec) open import Cubical.HITs.GroupoidTruncation as GT hiding (rec) -open import Cubical.HITs.Truncation variable ℓ ℓ' : Level -data K1 {ℓ : Level} (G : Group ℓ) : Type ℓ where - base : K1 G +data K[_,1] {ℓ : Level} (G : Group ℓ) : Type ℓ where + base : K[ G ,1] loop : ⟨ G ⟩ → base ≡ base loop-1g : loop (str G .GroupStr.1g) ≡ refl - loop-∙ : (x y : ⟨ G ⟩) → loop (str G .GroupStr._·_ x y) ≡ loop y ∙ loop x + loop-∙ : (x y : ⟨ G ⟩) → loop (G .snd .GroupStr._·_ x y) ≡ loop y ∙ loop x + squash : (x y : K[ G ,1]) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s + +module _ where + open import Cubical.HITs.S1 renaming (base to S¹-base; loop to S¹-loop) + open import Cubical.Data.Int + open import Cubical.Algebra.Group.Instances.Int + + test : S¹ ≃ K[ ℤGroup ,1] + test = isoToEquiv (iso f g {! !} {! !}) where + loop^_ : ℤ → S¹-base ≡ S¹-base + loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop + loop^ pos zero = refl + loop^ negsuc zero = sym S¹-loop + loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop + + Code1 : S¹ → Type + Code1 S¹-base = ℤ + Code1 (S¹-loop i) = sucPathℤ i + + -- f : S¹ → K[ ℤGroup ,1] + -- f S¹-base = base + -- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i + + f : S¹ → K[ ℤGroup ,1] + f S¹-base = base + f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i + + g : K[ ℤGroup ,1] → S¹ + g base = S¹-base + g (loop x i) = {! !} + g (loop-1g i i₁) = {! !} + g (loop-∙ x y i i₁) = {! !} + g (squash x x₁ p q r s i i₁ i₂) = {! !} + + +module _ (G : Group ℓ) where + open GroupStr (G .snd) -K[_,1] : (G : Group ℓ) → Type ℓ -K[ G ,1] = ∥ K1 G ∥₃ ------------------------------------------------------------------------------- -- Properties @@ -42,37 +77,56 @@ K[ G ,1] = ∥ K1 G ∥₃ module _ (G : Group ℓ) where open GroupStr (G .snd) + _⊙_ = _·_ + K[G,1] = K[ G ,1] K[G,1]∙ : Pointed ℓ - K[G,1]∙ = K[G,1] , ∣ base ∣₃ + K[G,1]∙ = K[G,1] , base ΩK[G,1] = Ω K[G,1]∙ π1K[G,1] = π 1 K[G,1]∙ - -- Since K[G, 1] is a 1-type, then all loops in K[G, 1] are identical - lemma1 : isOfHLevel 3 K[ G ,1] - lemma1 = {! !} + lemma1 : isOfHLevel 3 K[G,1] + lemma1 = squash lemma2 : isOfHLevel 2 ⟨ ΩK[G,1] ⟩ - lemma2 x y p q i j k = {! !} + lemma2 = squash base base + + ΩSetG : Pointed (ℓ-suc ℓ) + ΩSetG = (hSet ℓ) , (fst G) , is-set + + module Codes-aux where + f : (g : ⟨ G ⟩) → ⟨ G ⟩ ≃ ⟨ G ⟩ + f x = isoToEquiv (iso (λ y → y ⊙ x) (λ y → y ⊙ inv x) fg gf) where + fg : section (λ y → y ⊙ x) (λ y → y ⊙ inv x) + fg b = sym (·Assoc b (inv x) x) ∙ cong (b ⊙_) (·InvL x) ∙ ·IdR b + gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x) + gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a + + f1≡id : f 1g ≡ idEquiv ⟨ G ⟩ + f1≡id i = fnEq i , isEquivEq i where + fnEq : f 1g .fst ≡ idEquiv ⟨ G ⟩ .fst + fnEq i x = ·IdR x i + + isEquivEq : PathP (λ i → isEquiv (fnEq i)) (f 1g .snd) (idEquiv ⟨ G ⟩ .snd) + isEquivEq = toPathP (isPropIsEquiv (idfun ⟨ G ⟩) (subst isEquiv fnEq (f 1g .snd)) (idEquiv ⟨ G ⟩ .snd)) Codes : K[G,1] → hSet ℓ - Codes = GT.rec isGroupoidHSet Codes' where - CodesFunc : ⟨ G ⟩ → ⟨ G ⟩ ≡ ⟨ G ⟩ - CodesFunc g = {! g !} + Codes base = ⟨ G ⟩ , is-set + Codes (loop x i) = {! !} + Codes (loop-1g i i₁) = {! !} + Codes (loop-∙ x y i i₁) = {! !} + Codes (squash x x₁ p q r s i i₁ i₂) = {! !} - Codes' : K1 G → hSet ℓ - Codes' base = ⟨ G ⟩ , is-set - Codes' (loop x i) = ⟨ G ⟩ , is-set - Codes' (loop-1g i i₁) = {! !} - Codes' (loop-∙ x y i i₁) = {! !} - - encode : (z : K[G,1]) → ∣ base ∣₃ ≡ z → ⟨ Codes z ⟩ - encode z p = {! !} + encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩ + encode z p = subst (λ x → Codes x .fst) p 1g decode : ⟨ G ⟩ → base ≡ base - decode = loop + decode x = loop x + + encode-decode : (z : ⟨ G ⟩) → encode base (decode z) ≡ z + encode-decode z = {! !} ΩKG1≃G' : GroupIso {! ΩK[G,1] !} G @@ -81,12 +135,12 @@ module _ (G : Group ℓ) where f : ⟨ ΩK[G,1] ⟩ → ⟨ G ⟩ f p = {! !} - ΩKG1-idem-trunc : π 1 (K[ G ,1] , ∣ base ∣₃) ≃ ⟨ ΩK[G,1] ⟩ + ΩKG1-idem-trunc : π 1 (K[G,1]∙) ≃ ⟨ ΩK[G,1] ⟩ ΩKG1-idem-trunc = isoToEquiv (setTruncIdempotentIso lemma2) - π₁KG1≃G : ⟨ πGr 0 (K[ G ,1] , ∣ base ∣₃) ⟩ ≃ ⟨ G ⟩ + π₁KG1≃G : ⟨ πGr 0 (K[G,1]∙) ⟩ ≃ ⟨ G ⟩ π₁KG1≃G = compEquiv ΩKG1-idem-trunc ΩKG1≃G - + -- Uniqueness - + module _ (n : ℕ) (X Y : Pointed ℓ) where \ No newline at end of file