From 8fdbe83f8dbb13a6827ea79a2407167da81af350 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 22 Nov 2024 11:45:50 -0600 Subject: [PATCH] wip --- src/Misc/FiveLemma/Group/ExactSequence.agda | 32 ++++- src/Misc/STLCLogRel.agda | 135 ++++++++++++++++++++ src/ThesisWork/EMSpace.agda | 42 ++++++ 3 files changed, 208 insertions(+), 1 deletion(-) create mode 100644 src/Misc/STLCLogRel.agda create mode 100644 src/ThesisWork/EMSpace.agda diff --git a/src/Misc/FiveLemma/Group/ExactSequence.agda b/src/Misc/FiveLemma/Group/ExactSequence.agda index 0b2125f..9c545b7 100644 --- a/src/Misc/FiveLemma/Group/ExactSequence.agda +++ b/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 = {! !} \ No newline at end of file diff --git a/src/Misc/STLCLogRel.agda b/src/Misc/STLCLogRel.agda new file mode 100644 index 0000000..e1d4eb4 --- /dev/null +++ b/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) diff --git a/src/ThesisWork/EMSpace.agda b/src/ThesisWork/EMSpace.agda new file mode 100644 index 0000000..cae0637 --- /dev/null +++ b/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 {! !} {! !} {! !}