show that K is strong pre-Elgot

src/Category/Construction/PreElgotMonads.lagda.md

@@ -17,7 +17,7 @@ open import Categories.Category.Core
 ```agda
 module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
 open Ambient ambient
-open import Monad.ElgotMonad ambient
+open import Monad.PreElgot ambient
 open import Algebra.ElgotAlgebra ambient
 open HomReasoning
 open Equiv

src/Misc/Monad/Elgot.lagda.md

@@ -1,7 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 open import Level
 open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.Monad.Construction.Kleisli
@@ -11,54 +9,16 @@ open import Categories.Functor
 ```
 -->
 
-## Summary
-This file introduces Elgot Monads.
-
-TODO: Probably only Pre-Elgot is needed
-
-- [X] *Definition 13* Pre-Elgot Monads
-- [ ] *Definition 13* strong pre-Elgot
-- [X] *Definition 14* Elgot Monads
-- [ ] *Definition 14* strong Elgot
-- [ ] *Proposition 15* (Strong) Elgot monads are (strong) pre-Elgot
-
-## Code
-
 ```agda
-module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
+module Misc.Monad.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open HomReasoning
   open MR C
   open Equiv
   open import Algebra.ElgotAlgebra ambient
+  open import Monad.PreElgot ambient
 ```
 
-### *Definition 13*: Pre-Elgot Monads
-
-```agda
-  record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
-    open Monad T
-    open RMonad (Monad⇒Kleisli C T) using (extend)
-    open Functor F renaming (F₀ to T₀; F₁ to T₁)
-
-    -- every TX needs to be equipped with an elgot algebra structure
-    field
-      elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
-
-    module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
-
-    -- with the following associativity
-    field
-      pres : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
-        → elgotalgebras._# ((extend h +₁ idC) ∘ f) ≈ extend h ∘ (elgotalgebras._# {X}) f
-  
-  record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
-    field
-      T : Monad C
-      isPreElgot : IsPreElgot T
-
-    open IsPreElgot isPreElgot public
-```
 ### *Definition 14*: Elgot Monads
 
 ```agda
@@ -90,7 +50,7 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
     open IsElgot isElgot public
 ```
 
-### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot
+### *Proposition 15*: Elgot monads are pre-Elgot
 
   -- elgot monads are pre-elgot
   Elgot⇒PreElgot : ElgotMonad → PreElgotMonad

src/Monad/Instance/K/Commutative.lagda.md

@@ -22,7 +22,7 @@ open import Category.Construction.UniformIterationAlgebras ambient
 open import Algebra.UniformIterationAlgebra ambient
 open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 open import Algebra.ElgotAlgebra ambient
-open import Monad.Instance.K.Compositionality ambient MK
+open import Monad.Instance.K.Elgot ambient MK
 
 open Equiv
 open HomReasoning

src/Monad/Instance/K/Elgot.lagda.md

@@ -1,5 +1,3 @@
-# TODO: every KX satisfies compositionality
-
 ```agda
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Level
@@ -8,8 +6,10 @@ open import Category.Instance.AmbientCategory
 import Monad.Instance.K as MIK
 ```
 
+# Every KX is a free Elgot algebra
+
 ```agda
-module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
+module Monad.Instance.K.Elgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
   open Ambient ambient
   open MIK ambient
   open MonadK MK

src/Monad/Instance/K/PreElgot.lagda.md

@@ -20,9 +20,9 @@ open MIK ambient
 open MonadK MK
 open import Algebra.ElgotAlgebra ambient
 open import Algebra.UniformIterationAlgebra ambient
-open import Monad.ElgotMonad ambient
+open import Monad.PreElgot ambient
 open import Monad.Instance.K ambient
-open import Monad.Instance.K.Compositionality ambient MK
+open import Monad.Instance.K.Elgot ambient MK
 open import Monad.Instance.K.Commutative ambient MK
 open import Monad.Instance.K.Strong ambient MK
 open import Category.Construction.PreElgotMonads ambient
@@ -37,22 +37,22 @@ open M C
 # K is a pre-Elgot monad
 
 ```agda
--- TODO fix global declarations on Commutative.lagda.md
--- open Elgot-Algebra-on using (#-Compositionality)
--- TODO fix this import mess!!!
--- _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
-
 isPreElgot : IsPreElgot monadK
 isPreElgot = record
   { elgotalgebras = λ {X} → elgot X
-  ; pres = λ f h → sym (extend-preserve h f)
+  ; extend-preserves = λ f h → sym (extend-preserve h f)
   }
   where open kleisliK using (extend)
 
 preElgot : PreElgotMonad
 preElgot = record { T = monadK ; isPreElgot = isPreElgot }
 
--- initialPreElgot :
+strongPreElgot : IsStrongPreElgot KStrong
+strongPreElgot = record 
+  { preElgot = isPreElgot 
+  ; strengthen-preserves = τ-comm 
+  }
+
 initialPreElgot : IsInitial PreElgotMonads preElgot
 initialPreElgot = record
   { ! = !′
@@ -67,108 +67,112 @@ initialPreElgot = record
         })
       ; α-η = FreeObject.*-lift (freealgebras _) (T.η.η _)
       ; α-μ = α-μ
-      ; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) (T.η.η B))
+      ; preserves = λ {X} {B} f → Elgot-Algebra-Morphism.preserves (((freeElgot B) FreeObject.*) {A = record { A = T.F.F₀ B ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η B))
       }
       where
         open PreElgotMonad A using (T)
         open RMonad (Monad⇒Kleisli C T) using (extend)
         module T = Monad T
-        open PreElgotMonad preElgot using ()
         open monadK using () renaming (η to ηK; μ to μK)
         open Elgot-Algebra-on using (#-resp-≈)
+        T-Alg : ∀ (X : Obj) → Elgot-Algebra
+        T-Alg X = record { A = T.F.₀ X ; algebra = PreElgotMonad.elgotalgebras A }
+        K-Alg : ∀ (X : Obj) → Elgot-Algebra
+        K-Alg X = record { A = K.₀ X ; algebra = elgot X }
         η' : ∀ (X : Obj) → K.₀ X ⇒ T.F.₀ X
-        η' X = Elgot-Algebra-Morphism.h (_* {A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} (T.η.η X))
+        η' X = Elgot-Algebra-Morphism.h (_* {A = T-Alg X} (T.η.η X))
           where open FreeObject (freeElgot X)
-        commute : ∀ {X Y : Obj} (f : X ⇒ Y) → η' Y ∘ K.₁ f ≈ T.F.₁ f ∘ η' X
-        commute {X} {Y} f = begin
-          η' Y ∘ K.₁ f ≈⟨ *-uniq (T.F.₁ f ∘ T.η.η X) (record { h = η' Y ∘ K.₁ f ; preserves = pres₁ }) (begin
-            (η' Y ∘ K.₁ f) ∘ η ≈⟨ pullʳ (K₁η f) ⟩
-            η' Y ∘ ηK.η _ ∘ f ≈⟨ pullˡ (FreeObject.*-lift (freealgebras Y) (T.η.η Y)) ⟩
-            T.η.η Y ∘ f ≈⟨ NaturalTransformation.commute T.η f ⟩
-            T.F.₁ f ∘ T.η.η X ∎) ⟩
-          Elgot-Algebra-Morphism.h (_* {A = record { A = T.F.F₀ Y ; algebra = PreElgotMonad.elgotalgebras A }} (T.F.₁ f ∘ T.η.η _)) ≈⟨ sym (*-uniq (T.F.₁ f ∘ T.η.η X) (record { h = T.F.₁ f ∘ η' X ; preserves = pres₂ }) (begin
-            (T.F.₁ f ∘ η' X) ∘ η ≈⟨ pullʳ (FreeObject.*-lift (freealgebras X) (T.η.η X)) ⟩
-            T.F.₁ f ∘ T.η.η X ∎)) ⟩
-          T.F.₁ f ∘ η' X ∎
-          where
-            open FreeObject (freeElgot X)
         _#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f
         _#T = λ {B} {C} f → PreElgotMonad.elgotalgebras._# A {B} {C} f
+        -- some preservation facts that follow immediately, since these things are elgot-algebra-morphisms.
+        K₁-preserves : ∀ {X Y Z : Obj} (f : X ⇒ Y) (g : Z ⇒ K.₀ X + Z) → K.₁ f ∘ (g #K) ≈ ((K.₁ f +₁ idC) ∘ g) #K
+        K₁-preserves {X} {Y} {Z} f g = Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) {A = K-Alg Y} (ηK.η _ ∘ f))
+        μK-preserves : ∀ {X Y : Obj} (g : Y ⇒ K.₀ (K.₀ X) + Y) → μK.η X ∘ g #K ≈ ((μK.η X +₁ idC) ∘ g) #K
+        μK-preserves {X} g = Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) {A = K-Alg X} idC)
+        η'-preserves : ∀ {X Y : Obj} (g : Y ⇒ K.₀ X + Y) → η' X ∘ g #K ≈ ((η' X +₁ idC) ∘ g) #T
+        η'-preserves {X} g = Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) {A = T-Alg X} (T.η.η X))
+        commute : ∀ {X Y : Obj} (f : X ⇒ Y) → η' Y ∘ K.₁ f ≈ T.F.₁ f ∘ η' X
+        commute {X} {Y} f = begin
+          η' Y ∘ K.₁ f                                                    ≈⟨ FreeObject.*-uniq
+                                                                                (freeElgot X)
+                                                                                {A = T-Alg Y} 
+                                                                                (T.F.₁ f ∘ T.η.η X) 
+                                                                                (record { h = η' Y ∘ K.₁ f ; preserves = pres₁ }) 
+                                                                                comm₁ ⟩
+          Elgot-Algebra-Morphism.h (FreeObject._* (freeElgot X) {A = T-Alg Y} (T.F.₁ f ∘ T.η.η _)) ≈⟨ sym (FreeObject.*-uniq 
+                                                                                  (freeElgot X)
+                                                                                  {A = T-Alg Y} 
+                                                                                  (T.F.₁ f ∘ T.η.η X) 
+                                                                                  (record { h = T.F.₁ f ∘ η' X ; preserves = pres₂ }) 
+                                                                                  (pullʳ (FreeObject.*-lift (freealgebras X) (T.η.η X)))) ⟩
+          T.F.₁ f ∘ η' X                                                  ∎
+          where
             pres₁ : ∀ {Z} {g : Z ⇒ K.₀ X + Z} → (η' Y ∘ K.₁ f) ∘ g #K ≈ ((η' Y ∘ K.₁ f +₁ idC) ∘ g) #T
             pres₁ {Z} {g} = begin
-              (η' Y ∘ K.₁ f) ∘ (g #K) ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (ηK.η Y ∘ f))) ⟩
+              (η' Y ∘ K.₁ f) ∘ (g #K)                   ≈⟨ pullʳ (K₁-preserves f g) ⟩
-              η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K) ≈⟨ Elgot-Algebra-Morphism.preserves (((freeElgot Y) FreeObject.*) {A = record
+              η' Y ∘ (((K.₁ f +₁ idC) ∘ g) #K)          ≈⟨ η'-preserves ((K.₁ f +₁ idC) ∘ g) ⟩
-                                                                                                                        { A = T.F.F₀ Y
-                                                                                                                        ; algebra =
-                                                                                                                            record
-                                                                                                                            { _# = λ {X = X₁} → A PreElgotMonad.elgotalgebras.#
-                                                                                                                            ; #-Fixpoint = PreElgotMonad.elgotalgebras.#-Fixpoint A
-                                                                                                                            ; #-Uniformity = PreElgotMonad.elgotalgebras.#-Uniformity A
-                                                                                                                            ; #-Folding = PreElgotMonad.elgotalgebras.#-Folding A
-                                                                                                                            ; #-resp-≈ = PreElgotMonad.elgotalgebras.#-resp-≈ A
-                                                                                                                            }
-                                                                                                                        }} (T.η.η Y)) ⟩
               (((η' Y +₁ idC) ∘ (K.₁ f +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
               ((η' Y ∘ K.₁ f +₁ idC) ∘ g) #T            ∎
             pres₂ : ∀ {Z} {g : Z ⇒ K.₀ X + Z} → (T.F.₁ f ∘ η' X) ∘ g #K ≈ ((T.F.₁ f ∘ η' X +₁ idC) ∘ g) #T
             pres₂ {Z} {g} = begin
-              (T.F.₁ f ∘ η' X) ∘ g #K ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (T.η.η X))) ⟩
+              (T.F.₁ f ∘ η' X) ∘ g #K                                  ≈⟨ pullʳ (η'-preserves g) ⟩
               T.F.₁ f ∘ ((η' X +₁ idC) ∘ g) #T                         ≈⟨ (sym (F₁⇒extend T f)) ⟩∘⟨refl ⟩
-              extend (T.η.η Y ∘ f) ∘ ((η' X +₁ idC) ∘ g) #T ≈⟨ sym (PreElgotMonad.pres A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩
+              extend (T.η.η Y ∘ f) ∘ ((η' X +₁ idC) ∘ g) #T            ≈⟨ sym (PreElgotMonad.extend-preserves A ((η' X +₁ idC) ∘ g) (T.η.η Y ∘ f)) ⟩
               (((extend (T.η.η Y ∘ f) +₁ idC) ∘ (η' X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((F₁⇒extend T f) ⟩∘⟨refl) identity²)) ⟩
               ((T.F.₁ f ∘ η' X +₁ idC) ∘ g) #T                         ∎
+            comm₁ : (η' Y ∘ K.₁ f) ∘ _ ≈ T.F.₁ f ∘ T.η.η X
+            comm₁ = begin
+              (η' Y ∘ K.₁ f) ∘ _ ≈⟨ pullʳ (K₁η f) ⟩
+              η' Y ∘ ηK.η _ ∘ f  ≈⟨ pullˡ (FreeObject.*-lift (freealgebras Y) (T.η.η Y)) ⟩
+              T.η.η Y ∘ f        ≈⟨ NaturalTransformation.commute T.η f ⟩
+              T.F.₁ f ∘ T.η.η X  ∎
         α-μ : ∀ {X : Obj} → η' X ∘ μK.η X ≈ T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)
         α-μ {X} = begin
-          η' X ∘ μK.η X ≈⟨ FreeObject.*-uniq (freeElgot (K.₀ X)) (η' X) (record { h = η' X ∘ μK.η X ; preserves = pres₁ }) (cancelʳ monadK.identityʳ) ⟩
+          η' X ∘ μK.η X                                                                      ≈⟨ FreeObject.*-uniq 
-          Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = record
+                            (freeElgot (K.₀ X)) 
-                                                                              { A = T.F.F₀ X
+                            {A = T-Alg X} 
-                                                                              ; algebra =
+                            (η' X) 
-                                                                                  record
+                            (record { h = η' X ∘ μK.η X ; preserves = pres₁ }) 
-                                                                                  { _# = λ Z → (A PreElgotMonad.elgotalgebras.#) Z
+                            (cancelʳ monadK.identityʳ) ⟩
-                                                                                  ; #-Fixpoint = PreElgotMonad.elgotalgebras.#-Fixpoint A
+          Elgot-Algebra-Morphism.h (((freeElgot (K.₀ X)) FreeObject.*) {A = T-Alg X} (η' X)) ≈⟨ sym (FreeObject.*-uniq 
-                                                                                  ; #-Uniformity = PreElgotMonad.elgotalgebras.#-Uniformity A
+                                                                                                      (freeElgot (K.₀ X)) 
-                                                                                  ; #-Folding = PreElgotMonad.elgotalgebras.#-Folding A
+                                                                                                      {A = T-Alg X} 
-                                                                                  ; #-resp-≈ = PreElgotMonad.elgotalgebras.#-resp-≈ A
+                                                                                                      (η' X) 
-                                                                                  }
+                                                                                                      (record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ }) 
-                                                                              }} (η' X)) ≈⟨ sym (FreeObject.*-uniq (freeElgot (K.₀ X)) (η' X) (record { h = T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) ; preserves = pres₂ }) (begin
+                                                                                                      comm) ⟩
-            (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈⟨ (refl⟩∘⟨ sym (commute (η' X))) ⟩∘⟨refl ⟩
-            (T.μ.η X ∘ η' _ ∘ K.₁ (η' X)) ∘ ηK.η (K.₀ X) ≈⟨ assoc ○ refl⟩∘⟨ (assoc ○  refl⟩∘⟨ sym (monadK.η.commute (η' X))) ⟩
-            T.μ.η X ∘ η' _ ∘ ηK.η (T.F.F₀ X) ∘ η' X ≈⟨ refl⟩∘⟨ (pullˡ (FreeObject.*-lift (freealgebras _) (T.η.η _))) ⟩
-            T.μ.η X ∘ T.η.η _ ∘ η' X ≈⟨ cancelˡ (Monad.identityʳ T) ⟩
-            η' X ∎)) ⟩
           T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)                                                ∎
           where
-            _#K = λ {B} {C} f → Elgot-Algebra._# (FreeObject.FX (freeElgot C)) {B} f
-            _#T = λ {B} {C} f → PreElgotMonad.elgotalgebras._# A {B} {C} f
             pres₁ : ∀ {Z} {g : Z ⇒ K.₀ (K.₀ X) + Z} → (η' X ∘ μK.η X) ∘ g #K ≈ ((η' X ∘ μK.η X +₁ idC) ∘ g) #T
             pres₁ {Z} {g} = begin
-              (η' X ∘ μK.η X) ∘ (g #K) ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) idC)) ⟩
+              (η' X ∘ μK.η X) ∘ (g #K)                   ≈⟨ pullʳ (μK-preserves g) ⟩
-              η' X ∘ ((μK.η X +₁ idC) ∘ g) #K ≈⟨ Elgot-Algebra-Morphism.preserves (((freeElgot X) FreeObject.*) (T.η.η X)) ⟩
+              η' X ∘ ((μK.η X +₁ idC) ∘ g) #K            ≈⟨ η'-preserves ((μK.η X +₁ idC) ∘ g) ⟩
               (((η' X +₁ idC) ∘ (μK.η X +₁ idC) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
               (((η' X ∘ μK.η X +₁ idC) ∘ g) #T)          ∎
             pres₂ : ∀ {Z} {g : Z ⇒ K.₀ (K.₀ X) + Z} → (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ g #K ≈ ((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T
             pres₂ {Z} {g} = begin
-              (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ (g #K) ≈⟨ pullʳ (pullʳ (Elgot-Algebra-Morphism.preserves (((freeElgot (K.₀ X)) FreeObject.*) (T.η.η (K.₀ X))))) ⟩
+              (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ (g #K)                                      ≈⟨ pullʳ (pullʳ (η'-preserves g)) ⟩
-              T.μ.η X ∘ T.F.₁ (η' X) ∘ (((η' (K.₀ X) +₁ idC) ∘ g) #T) ≈⟨ refl⟩∘⟨ ((sym (F₁⇒extend T (η' X))) ⟩∘⟨refl ○ sym (PreElgotMonad.pres A ((η' (K.₀ X) +₁ idC) ∘ g) (T.η.η (T.F.F₀ X) ∘ η' X)) )⟩
+              T.μ.η X ∘ T.F.₁ (η' X) ∘ (((η' (K.₀ X) +₁ idC) ∘ g) #T)                             ≈⟨ refl⟩∘⟨ ((sym (F₁⇒extend T (η' X))) ⟩∘⟨refl ○ sym (PreElgotMonad.extend-preserves A ((η' (K.₀ X) +₁ idC) ∘ g) (T.η.η (T.F.F₀ X) ∘ η' X)) )⟩
-              T.μ.η X ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ (sym μ-extend) ⟩∘⟨refl ⟩
+              T.μ.η X ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T               ≈⟨ (sym (elimʳ T.F.identity)) ⟩∘⟨refl ⟩
-              extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T ≈⟨ sym (PreElgotMonad.pres A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘
+              extend idC ∘ ((extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T            ≈⟨ sym (PreElgotMonad.extend-preserves A ((extend (T.η.η (T.F.F₀ X) ∘ η' X) +₁ idC) ∘ (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩
-                                                                                                                      (η' (K.₀ X) +₁ idC) ∘ g) idC) ⟩
+              (((extend idC +₁ idC) ∘ (extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((elimʳ T.F.identity) ⟩∘⟨ (F₁⇒extend T (η' X))) identity²)) ⟩
-              (((extend idC +₁ idC) ∘ (extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (μ-extend ⟩∘⟨ (F₁⇒extend T (η' X))) identity²)) ⟩
               (((T.μ.η X ∘ T.F.₁ (η' X) +₁ idC) ∘ (η' _ +₁ idC) ∘ g) #T)                          ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity²)) ⟩
               (((T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X) +₁ idC) ∘ g) #T)                             ∎
-              where
+            comm : (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈ η' X
-                μ-extend : extend idC ≈ T.μ.η X
+            comm = begin
-                μ-extend = begin
+              (T.μ.η X ∘ T.F.₁ (η' X) ∘ η' (K.₀ X)) ∘ ηK.η (K.₀ X) ≈⟨ (refl⟩∘⟨ sym (commute (η' X))) ⟩∘⟨refl ⟩
-                  T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩
+              (T.μ.η X ∘ η' _ ∘ K.₁ (η' X)) ∘ ηK.η (K.₀ X)         ≈⟨ assoc ○ refl⟩∘⟨ (assoc ○  refl⟩∘⟨ sym (monadK.η.commute (η' X))) ⟩
-                  T.μ.η X ∎
+              T.μ.η X ∘ η' _ ∘ ηK.η (T.F.F₀ X) ∘ η' X              ≈⟨ refl⟩∘⟨ (pullˡ (FreeObject.*-lift (freealgebras _) (T.η.η _))) ⟩
+              T.μ.η X ∘ T.η.η _ ∘ η' X                             ≈⟨ cancelˡ (Monad.identityʳ T) ⟩
+              η' X                                                 ∎
     !-unique′ : ∀ {A : PreElgotMonad} (f : PreElgotMonad-Morphism preElgot A) → PreElgotMonad-Morphism.α (!′ {A = A}) ≃ PreElgotMonad-Morphism.α f
-    !-unique′ {A} f {X} = sym (*-uniq (T.η.η X) (record
+    !-unique′ {A} f {X} = sym (FreeObject.*-uniq
-                                                  { h = α.η X
+                                (freeElgot X) 
-                                                  ; preserves = preserves _
+                                {A = record { A = T.F.F₀ X ; algebra = PreElgotMonad.elgotalgebras A }} 
-                                                  }) α-η)
+                                (T.η.η X) 
+                                (record { h = α.η X ; preserves = preserves _ }) 
+                                α-η)
       where
         open PreElgotMonad-Morphism f using (α; α-η; preserves)
         open PreElgotMonad A using (T)
         module T = Monad T
-        open FreeObject (freeElgot X)
 ```

src/Monad/PreElgot.lagda.md

@@ -0,0 +1,73 @@
+<!--
+```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Level
+open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.Monad.Construction.Kleisli
+open import Categories.Monad
+open import Categories.Monad.Strong
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Categories.Functor
+open import Data.Product using (_,_)
+```
+-->
+
+```agda
+module Monad.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open HomReasoning
+  open MR C
+  open Equiv
+  open import Algebra.ElgotAlgebra ambient
+```
+
+# (strong) pre-Elgot monads
+
+```agda
+  record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
+    open Monad T
+    open RMonad (Monad⇒Kleisli C T) using (extend)
+    open Functor F renaming (F₀ to T₀; F₁ to T₁)
+
+    -- every TX needs to be equipped with an elgot algebra structure
+    field
+      elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
+
+    module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
+
+    -- where kleisli lifting preserves iteration
+    field
+      extend-preserves : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
+        → elgotalgebras._# ((extend h +₁ idC) ∘ f) ≈ extend h ∘ elgotalgebras._# {X} f
+  
+  record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      T : Monad C
+      isPreElgot : IsPreElgot T
+
+    open IsPreElgot isPreElgot public
+
+  record IsStrongPreElgot (SM : StrongMonad monoidal) : Set (o ⊔ ℓ ⊔ e) where
+    open StrongMonad SM using (M; strengthen)
+    open Monad M using (F)
+
+    -- M is pre-Elgot
+    field
+      preElgot : IsPreElgot M
+    
+    open IsPreElgot preElgot public
+
+    -- and strength is iteration preserving
+    field
+      strengthen-preserves : ∀ {X Y Z} (f : Z ⇒ F.₀ Y + Z) 
+        → strengthen.η (X , Y) ∘ (idC ⁂ elgotalgebras._# f) ≈ elgotalgebras._# ((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))
+  
+  record StrongPreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      SM : StrongMonad monoidal
+      isStrongPreElgot : IsStrongPreElgot SM
+    
+    open IsStrongPreElgot isStrongPreElgot public
+```
+