🚧 Working on stable algebras, currently showing that K is strong

src/Algebra/Properties.lagda.md

@@ -39,9 +39,32 @@ This file contains some typedefs and records concerning different algebras.
   FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} uniformForgetfulF X
 ```
 
--- TODO this is an alternate characterization, prove it with lemma 18 and formalize definition 17
 ## Stable Free Uniform-Iteration Algebras
 
+```agda
+  record IsStableFreeUniformIterationAlgebra {Y : Obj} (freeAlgebra : FreeUniformIterationAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    open FreeObject freeAlgebra using (η) renaming (FX to FY)
+    open Uniform-Iteration-Algebra FY using (_#)
+
+    field
+        -- TODO awkward notation...
+        [_,_]♯ : ∀ {X : Obj} (A : Uniform-Iteration-Algebra) (f : X × Y ⇒ Uniform-Iteration-Algebra.A A) → X × Uniform-Iteration-Algebra.A FY ⇒ Uniform-Iteration-Algebra.A A
+        ♯-law : ∀ {X : Obj} {A : Uniform-Iteration-Algebra} (f : X × Y ⇒ Uniform-Iteration-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (idC ⁂ η)
+        ♯-preserving : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : X × Y ⇒ Uniform-Iteration-Algebra.A B) {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → [ B , f ]♯ ∘ (idC ⁂ h #) ≈ Uniform-Iteration-Algebra._# B (([ B , f ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
+        ♯-unique : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : X × Y ⇒ Uniform-Iteration-Algebra.A B) (g : X × Uniform-Iteration-Algebra.A FY ⇒ Uniform-Iteration-Algebra.A B)
+          → f ≈ g ∘ (idC ⁂ η)
+          → (∀ {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Uniform-Iteration-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
+          → g ≈ [ B , f ]♯
+
+  record StableFreeUniformIterationAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    field
+      Y : Obj
+      freeAlgebra : FreeUniformIterationAlgebra Y
+      isStableFreeUniformIterationAlgebra : IsStableFreeUniformIterationAlgebra freeAlgebra
+    
+    open IsStableFreeUniformIterationAlgebra isStableFreeUniformIterationAlgebra public
+```
+
 ## Free Elgot Algebras
 
 ```agda
@@ -61,21 +84,29 @@ This file contains some typedefs and records concerning different algebras.
 
 ## Stable Free Elgot Algebras
 
-**TODO** This can be defined, KY is the free elgot algebra and η is the morphism of the free object!
+-- TODO this is duplicated from uniform iteration and since free elgots coincide with free uniform iterations this can later be removed.
 ```agda
-  record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+  record IsStableFreeElgotAlgebra {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
-    field
-      Y : Obj
-      freeElgot : FreeElgotAlgebra Y
-      -- _♯ : ∀ {A : Elgot-Algebra} 
     open FreeObject freeElgot using (η) renaming (FX to FY)
     open Elgot-Algebra FY using (_#)
+
     field
         -- TODO awkward notation...
         [_,_]♯ : ∀ {X : Obj} (A : Elgot-Algebra) (f : X × Y ⇒ Elgot-Algebra.A A) → X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A A
         ♯-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (idC ⁂ η)
-        ♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → f ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
+        ♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B (([ B , f ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
-        -- TODO ♯ is unique iteration preserving
+        ♯-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) (g : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B)
+          → f ≈ g ∘ (idC ⁂ η)
+          → (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
+          → g ≈ [ B , f ]♯
+
+  record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    field
+      Y : Obj
+      freeElgot : FreeElgotAlgebra Y
+      isStableFreeElgotAlgebra : IsStableFreeElgotAlgebra freeElgot
+    
+    open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public
 ```
 
 ## Free Elgot to Free Uniform Iteration

src/Monad/Instance/K.lagda.md

@@ -2,11 +2,16 @@
 ```agda
 open import Level
 open import Categories.FreeObjects.Free
+open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
+open import Categories.Category
 open import Categories.Functor.Core
 open import Categories.Adjoint
 open import Categories.Adjoint.Properties
 open import Categories.Monad
+open import Categories.Monad.Strong
 open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.NaturalTransformation
+-- open import Data.Product using (_,_; Σ; Σ-syntax)
 ```
 -->
 
@@ -28,7 +33,8 @@ In this file I explore the monad ***K*** and its properties:
 module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open import Category.Construction.UniformIterationAlgebras ambient
-  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF)
+  open import Algebra.UniformIterationAlgebra
+  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 
   open Equiv
 
@@ -53,3 +59,52 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
     -- EilenbergMoore⇒UniformIterationAlgebras : StrongEquivalence (EilenbergMoore K) (Uniform-Iteration-Algebras D)
     -- EilenbergMoore⇒UniformIterationAlgebras = {!   !}
 ```
+
+### *Proposition 19* If the algebras are stable then K is strong
+
+```agda
+  record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+    field
+      algebras : ∀ X → FreeUniformIterationAlgebra X
+      stable : ∀ X → IsStableFreeUniformIterationAlgebra (algebras X)
+    
+    K : Monad C
+    K = MonadK.K (record { algebras = algebras })
+
+    open Monad K using (F)
+    open Functor F using () renaming (F₀ to K₀; F₁ to K₁)
+
+    KStrong : StrongMonad {C = C} monoidal
+    KStrong = record 
+      { M = K 
+      ; strength = record
+        { strengthen = ntHelper (record { η = τ ; commute = λ f → {!   !} }) 
+        ; identityˡ = {!   !}
+        ; η-comm = {!   !}
+        ; μ-η-comm = {!   !}
+        ; strength-assoc = {!   !}
+        }
+      }
+      where
+        open import Agda.Builtin.Sigma
+        open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving)
+
+        module _ (P : Category.Obj (CProduct C C)) where
+          η = λ Z → FreeObject.η (algebras Z)
+          [_,_,_]♯ = λ {A} X Y f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} Y f
+
+
+          X = fst P
+          Y = snd P
+          τ : X × K₀ Y ⇒ K₀ (X × Y)
+          τ = [ Y , FreeObject.FX (algebras (X × Y)) , η (X × Y) ]♯
+
+          τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
+          τ-η = sym (♯-law (stable Y) (η (X × Y)))
+
+        [_,_]# : ∀ (A : Uniform-Iteration-Algebra ambient) {X} → (X ⇒ ((Uniform-Iteration-Algebra.A A) + X)) → (X ⇒ Uniform-Iteration-Algebra.A A)
+        [ A , f ]# = Uniform-Iteration-Algebra._# A f
+
+        τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
+        τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h
+```