emspace

src/ThesisWork/EMSpace.agda

@@ -3,10 +3,14 @@
 module ThesisWork.EMSpace where
 
 open import Cubical.Algebra.Group
+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.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.Pointed
@@ -15,7 +19,8 @@ open import Cubical.Foundations.Structure
 open import Cubical.Homotopy.Loopspace
 open import Cubical.Homotopy.Group.Base
 open import Cubical.HITs.SetTruncation as ST hiding (rec)
-open import Cubical.HITs.Truncation as T hiding (rec)
+open import Cubical.HITs.GroupoidTruncation as GT hiding (rec)
+open import Cubical.HITs.Truncation
 
 variable
   ℓ ℓ' : Level
@@ -27,16 +32,61 @@ data K1 {ℓ : Level} (G : Group ℓ) : Type ℓ where
   loop-∙ : (x y : ⟨ G ⟩) → loop (str G .GroupStr._·_ x y) ≡ loop y ∙ loop x
 
 K[_,1] : (G : Group ℓ) → Type ℓ
-K[ G ,1] = ∥ K1 G ∥ 3
+K[ G ,1] = ∥ K1 G ∥₃
 
 -------------------------------------------------------------------------------
 -- Properties
 
 -- ΩK(G,1) ≃ G
 
-π₁KG1≃G : (G : Group ℓ) → GroupIso (πGr 0 (K[ G ,1] , ∣ base ∣)) G
-π₁KG1≃G G = {!   !} , {!   !} where
+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]∙
+  π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 = {!   !}
+
+  lemma2 : isOfHLevel 2 ⟨ ΩK[G,1] ⟩
+  lemma2 x y p q i j k = {!   !}
+
+  Codes : K[G,1] → hSet ℓ
+  Codes = GT.rec isGroupoidHSet Codes' where
+    CodesFunc : ⟨ G ⟩ → ⟨ G ⟩ ≡ ⟨ G ⟩
+    CodesFunc g = {! g  !}
+
+    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 = {!   !}
+
+  decode : ⟨ G ⟩ → base ≡ base
+  decode = loop
+
+  ΩKG1≃G' : GroupIso {! ΩK[G,1]  !} G
+
+  ΩKG1≃G : ⟨ ΩK[G,1] ⟩ ≃ ⟨ G ⟩
+  ΩKG1≃G = isoToEquiv (iso f {!   !} {!   !} {!   !}) where
+    f : ⟨ ΩK[G,1] ⟩ → ⟨ G ⟩
+    f p = {!   !}
+
+  ΩKG1-idem-trunc : π 1 (K[ G ,1] , ∣ base ∣₃) ≃ ⟨ ΩK[G,1] ⟩
+  ΩKG1-idem-trunc = isoToEquiv (setTruncIdempotentIso lemma2)
+
+  π₁KG1≃G : ⟨ πGr 0 (K[ G ,1] , ∣ base ∣₃) ⟩ ≃ ⟨ G ⟩
+  π₁KG1≃G = compEquiv ΩKG1-idem-trunc ΩKG1≃G
+  
 -- Uniqueness
-
+ 
 module _ (n : ℕ) (X Y : Pointed ℓ) where