emspace

src/Misc/STLCLogRel.agda

@@ -6,9 +6,12 @@ open import Data.Empty
 open import Data.Fin hiding (fold)
 open import Data.Maybe
 open import Data.Nat
-open import Data.Product
+open import Data.Irrelevant
+import Relation.Nullary using (Dec; yes; no)
+open import Data.Product.Base
 open import Data.Sum
 open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 id : {A : Set} → A → A
 id {A} x = x
@@ -18,17 +21,15 @@ data type : Set where
   bool : type
   _-→_ : type → type → type
   `_ : ℕ → type
-  μ_ : type → type
 
 data term : Set where
   `_ : ℕ → term
+  `unit : term
   `true : term
   `false : term
   `if_then_else_ : term → term → term → term
   `λ[_]_ : (τ : type) → (e : term) → term
   _∙_ : term → term → term
-  `fold : term → term
-  `unfold : term → term
 
 data ctx : Set where
   nil : ctx
@@ -48,7 +49,6 @@ type-subst bool v = bool
 type-subst (τ -→ τ₁) v = (type-subst τ v) -→ (type-subst τ₁ v)
 type-subst (` zero) v = v
 type-subst (` suc x) v = ` x
-type-subst (μ τ) v = μ (type-subst τ v)
 
 data sub : Set where
   nil : sub
@@ -57,38 +57,27 @@ data sub : Set where
 subst : term → term → term
 subst (` zero) v = v
 subst (` suc x) v = ` x
+subst `unit _ = `unit
 subst `true v = `true
 subst `false v = `false
 subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
 subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
 subst (x ∙ x₁) v = (subst x v) ∙ (subst x₁ v)
-subst (`fold x) v = `fold (subst x v)
-subst (`unfold x) v = `unfold (subst x v)
-
-data value-rel : type → term → Set where 
-  v-`true : value-rel bool `true
-  v-`false : value-rel bool `false
-  v-`λ[_]_ : ∀ {τ e} → value-rel τ (`λ[ τ ] e)
-  v-`fold : ∀ {τ e} → value-rel (type-subst τ (μ τ)) e → value-rel (μ τ) (`fold e)
-
-data good-subst : ctx → sub → Set where
-  nil : good-subst nil nil
-  cons : ∀ {ctx τ γ v}
-    → good-subst ctx γ
-    → value-rel τ v
-    → good-subst (cons ctx τ) γ
 
 data step : term → term → Set where
   step-if-1 : ∀ {e₁ e₂} → step (`if `true then e₁ else e₂) e₁
   step-if-2 : ∀ {e₁ e₂} → step (`if `false then e₁ else e₂) e₂
   step-`λ : ∀ {τ e v} → step ((`λ[ τ ] e) ∙ v) (subst e v)
-  step-`fold : ∀ {v} → step (`unfold (`fold v)) v
+  
+  -- TODO: Do I need these rules?
+  step-if : ∀ {e e' e₁ e₂} → step e e' → step (`if e then e₁ else e₂) (`if e' then e₁ else e₂)
 
 data steps : ℕ → term → term → Set where
   zero : ∀ {e} → steps zero e e
   suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''
 
 data _⊢_∶_ : ctx → term → type → Set where
+  type-`unit : ∀ {ctx} → ctx ⊢ `unit ∶ unit
   type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
   type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
   type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
@@ -107,29 +96,72 @@ data _⊢_∶_ : ctx → term → type → Set where
     → ctx ⊢ e₂ ∶ τ₂
     → ctx ⊢ (e₁ ∙ e₂) ∶ τ₂
 
-  type-`fold : ∀ {ctx τ e}
-    → ctx ⊢ e ∶ (type-subst τ (μ τ))
-    → ctx ⊢ (`fold e) ∶ (μ τ)
-  type-`unfold : ∀ {ctx τ e}
-    → ctx ⊢ e ∶ (μ τ)
-    → ctx ⊢ (`unfold e) ∶ (type-subst τ (μ τ))
-
 irreducible : term → Set
 irreducible e = ¬ (∃ λ e' → step e e')
 
-data term-relation : type → term → Set where
+data value-rel : type → term → Set
+data term-rel : type → term → Set
+
+safe : (e : term) → Set
+safe e = ∀ {e' : term} → {n : ℕ} → (steps n e e') → (Σ[ τ ∈ type ] (value-rel τ e')) ⊎ (∃ (λ e'' → step e' e''))
+
+data value-rel where 
+  v-`unit : value-rel unit `unit
+  v-`true : value-rel bool `true
+  v-`false : value-rel bool `false
+  v-`λ[_]_ : ∀ {τ₁ τ₂ e} → term-rel τ₂ e → value-rel (τ₁ -→ τ₂) (`λ[ τ₁ ] e)
+
+data good-subst : ctx → sub → Set where
+  nil : good-subst nil nil
+  cons : ∀ {ctx τ γ v}
+    → good-subst ctx γ
+    → value-rel τ v
+    → good-subst (cons ctx τ) γ
+
+data term-rel where
   e-term : ∀ {τ e}
     → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
-    → term-relation τ e
+    → term-rel τ e
 
-type-sound : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
-type-sound {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e''
+-- type-sound : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
+-- type-sound {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e''
 
 _⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
-_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-relation τ e
+_⊨_∶_ Γ e τ = (γ : sub) → good-subst Γ γ → term-rel τ e
 
-fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-sound well-typed → Γ ⊨ e ∶ τ
-fundamental {Γ} {e} {τ} well-typed type-sound γ good-sub = e-term f
-  where
-    f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'
-    f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (type-sound e' steps)
+fundamental : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Γ ⊨ e ∶ τ
+
+-- Semantic type soundness
+part1 : {e : term} → {τ : type} → nil ⊢ e ∶ τ → term-rel τ e
+part1 p =
+  let p' = fundamental p in
+  p' nil nil
+
+unit-irred : irreducible `unit
+unit-irred ()
+
+true-irred : irreducible `true
+true-irred ()
+
+false-irred : irreducible `false
+false-irred ()
+
+postulate
+  decide-irred : ∀ {Γ} {τ} {e} → Γ ⊢ e ∶ τ → Dec (irreducible e)
+
+part2 : {e : term} → {τ : type} → term-rel τ e → safe e
+part2 t s with res ← decide-irred {!   !} = {!   !}
+
+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
+  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
+  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-`x p) γ (cons {v = v} γ-good v-value) = e-term (λ e' s i → {!   !})
+fundamental (type-`λ p) = λ γ x → {!   !}
+fundamental (type-∙ p p₁) = {!   !}

src/ThesisWork/EMSpace.agda

@@ -3,18 +3,24 @@
 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
 open import Cubical.Foundations.Prelude
 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
@@ -26,17 +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 ∥₃
 
-π₁KG1≃G : (G : Group ℓ) → GroupIso (πGr 0 (K[ G ,1] , ∣ base ∣)) G
-π₁KG1≃G G = {!   !} , {!   !} where
+-------------------------------------------------------------------------------
+-- Properties
 
-module _ where
-  open import Cubical.HITs.S1
-  open import Cubical.Data.Int
-  open import Cubical.Algebra.Group.Instances.Int
+-- ΩK(G,1) ≃ G
 
-  K[Z,1]=S1 : K[ ℤGroup ,1] ≃ S¹
-  K[Z,1]=S1 = isoToEquiv (iso f {!   !} {!   !} {!   !}) where
-    f : K[ ℤGroup ,1] → S¹
-    f x = T.rec {!   !} {!   !} {!   !}
+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