wip

src/ThesisWork/EMSpace.agda

@@ -7,7 +7,7 @@ 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 hiding (_·_)
+open import Cubical.Data.Nat using (ℕ) 
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.GroupoidLaws
@@ -113,14 +113,21 @@ module _ (G : Group ℓ) where
       isEquivEq = toPathP (isPropIsEquiv (idfun ⟨ G ⟩) (subst isEquiv fnEq (f 1g .snd)) (idEquiv ⟨ G ⟩ .snd))
 
   Codes : K[G,1] → hSet ℓ
-  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 = GT.rec isGroupoidHSet Codes' where
+    CodesFunc : ⟨ G ⟩ → ⟨ G ⟩ ≃ ⟨ G ⟩
+    CodesFunc g = {!   !}
 
-  encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩
-  encode z p = subst (λ x → Codes x .fst) p 1g
+    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₁) = {!   !}
+
+  module _ where
+    _ : (x y : ⟨ G ⟩) → subst {! λ x → Codes x .snd  !} {!   !} {!   !} ≡ {!   !}
+
+  encode : (z : K[G,1]) → ∣ base ∣₃ ≡ z → ⟨ Codes z ⟩
+  encode z p = {!   !}
 
   decode : ⟨ G ⟩ → base ≡ base
   decode x = loop x