wip

src/Misc/FiveLemma/Group/ExactSequence.agda

@@ -5,11 +5,13 @@ module Misc.FiveLemma.Group.ExactSequence where
 open import Agda.Primitive
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.Morphisms
-open import Cubical.Data.Nat
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Data.Nat hiding (_·_)
 open import Data.Fin
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Isomorphism
 open import Misc.FiveLemma.Group.Exact
 open import Misc.FiveLemma.Group.Morphisms
 
@@ -34,3 +36,31 @@ InfiniteLES :
   → (homSeq : (n : ℕ) → GroupHom (groupSeq n) (groupSeq (suc n)))
   → Type ℓ
 InfiniteLES groupSeq homSeq = (m : ℕ) → isExact (homSeq m) (homSeq (suc m))
+
+module _ {A B : Group ℓ} (f : GroupHom A B) where
+  private
+    groupSeq : (n : Fin 3) → Group ℓ
+    groupSeq zero = UnitGroup
+    groupSeq (1+ zero) = A
+    groupSeq (2+ zero) = B
+
+    homSeq : (n : Fin 2) → GroupHom (groupSeq (inj1 n)) (groupSeq (suc n))
+    homSeq zero =
+      let open GroupStr (A .snd) in
+      (λ _ → 1g) ,
+      record {
+        pres· = λ x y → sym (·IdR 1g) ;
+        pres1 = refl ;
+        presinv = λ x → let z = sym (·IdL (inv 1g)) ∙ cong (_· inv 1g) (sym (·InvL 1g)) ∙ sym (·Assoc (inv 1g) 1g (inv 1g)) ∙ cong (inv 1g ·_) (·InvR 1g) ∙ ·InvL 1g in sym z
+      }
+    homSeq (1+ zero) = f
+
+  0AB≃Mono : FiniteLES groupSeq homSeq ≃ isMono f
+  0AB≃Mono = isoToEquiv (iso ff {! gg  !} {!   !} {!   !}) where
+    ff : FiniteLES groupSeq homSeq → isMono f
+    ff ses fx≡fy = {!   !}
+
+    gg : isMono f → FiniteLES groupSeq homSeq
+    gg fMono m a = isoToEquiv (iso {!   !} {!   !} {!   !} {!   !}) where
+      fff : isInKer (homSeq (1+ m)) a → isInIm' (homSeq (inj1 m)) a
+      fff a-in-ker = {!   !}

src/Misc/STLCLogRel.agda

@@ -0,0 +1,135 @@
+module Misc.STLCLogRel where
+
+open import Agda.Builtin.Sigma
+open import Data.Bool
+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.Sum
+open import Relation.Nullary
+
+id : {A : Set} → A → A
+id {A} x = x
+
+data type : Set where
+  unit : type
+  bool : type
+  _-→_ : type → type → type
+  `_ : ℕ → type
+  μ_ : type → type
+
+data term : Set where
+  `_ : ℕ → 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
+  cons : ctx → type → ctx
+
+lookup : ctx → ℕ → Maybe type
+lookup nil _ = nothing
+lookup (cons ctx₁ x) zero = just x 
+lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
+
+data type-sub : Set where
+  nil : type-sub
+
+type-subst : type → type → type
+type-subst unit v = unit
+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
+  cons : sub → term → sub
+
+subst : term → term → term
+subst (` zero) v = v
+subst (` suc x) v = ` x
+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
+
+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-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
+  type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
+  type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
+    → ctx ⊢ e ∶ bool
+    → ctx ⊢ e₁ ∶ τ
+    → ctx ⊢ e₂ ∶ τ
+    → ctx ⊢ (`if e then e₁ else e₂) ∶ τ
+  type-`x : ∀ {ctx x}
+    → (p : Is-just (lookup ctx x))
+    → ctx ⊢ (` x) ∶ (to-witness p)
+  type-`λ : ∀ {ctx τ τ₂ e}
+    → (cons ctx τ) ⊢ e ∶ τ₂
+    → ctx ⊢ (`λ[ τ ] e) ∶ (τ -→ τ₂)
+  type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
+    → ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
+    → 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
+  e-term : ∀ {τ e}
+    → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
+    → term-relation τ 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
+
+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)

src/ThesisWork/EMSpace.agda

@@ -0,0 +1,42 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.EMSpace where
+
+open import Cubical.Algebra.Group
+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.Equiv
+open import Cubical.Foundations.Isomorphism
+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)
+
+variable
+  ℓ ℓ' : Level
+
+data K1 {ℓ : Level} (G : Group ℓ) : Type ℓ where
+  base : K1 G
+  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
+
+K[_,1] : (G : Group ℓ) → Type ℓ
+K[ G ,1] = ∥ K1 G ∥ 3
+
+π₁KG1≃G : (G : Group ℓ) → GroupIso (πGr 0 (K[ G ,1] , ∣ base ∣)) G
+π₁KG1≃G G = {!   !} , {!   !} where
+
+module _ where
+  open import Cubical.HITs.S1
+  open import Cubical.Data.Int
+  open import Cubical.Algebra.Group.Instances.Int
+
+  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 {!   !} {!   !} {!   !}