proved: f(1)≡id in EMSpace

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₁) = {!   !}
+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 = {!   !}

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