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/PreElgot.lagda.md

@@ -20,7 +20,7 @@ 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.Elgot ambient MK
 open import Monad.Instance.K.Commutative ambient MK
@@ -40,13 +40,19 @@ open M C
 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 }
 
+strongPreElgot : IsStrongPreElgot KStrong
+strongPreElgot = record 
+  { preElgot = isPreElgot 
+  ; strengthen-preserves = τ-comm 
+  }
+
 initialPreElgot : IsInitial PreElgotMonads preElgot
 initialPreElgot = record
   { ! = !′
@@ -111,7 +117,7 @@ initialPreElgot = record
             pres₂ {Z} {g} = begin
               (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
@@ -145,9 +151,9 @@ initialPreElgot = record
             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ʳ (η'-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 (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) ∘ (η' (K.₀ X) +₁ idC) ∘ g) 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) ⟩
               (((extend idC +₁ idC) ∘ (extend (T.η.η _ ∘ η' _) +₁ idC) ∘ ((η' _ +₁ idC)) ∘ g) #T) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ ((elimʳ T.F.identity) ⟩∘⟨ (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)                             ∎

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
+```
+