Work on initial pre-Elgot

src/Category/Construction/PreElgotMonads.lagda.md

@@ -18,6 +18,7 @@ open import Categories.Category.Core
 module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
 open Ambient ambient
 open import Monad.ElgotMonad ambient
+open import Algebra.ElgotAlgebra ambient
 open HomReasoning
 open Equiv
 open M C
@@ -25,12 +26,14 @@ open MR C
 
 module _ (P S : PreElgotMonad) where
   private
-    open PreElgotMonad P using () renaming (T to TP)
+    open PreElgotMonad P using () renaming (T to TP; elgotalgebras to P-elgots)
-    open PreElgotMonad S using () renaming (T to TS)
+    open PreElgotMonad S using () renaming (T to TS; elgotalgebras to S-elgots)
     module TP = Monad TP
     module TS = Monad TS
     open RMonad (Monad⇒Kleisli C TP) using () renaming (extend to extendP)
     open RMonad (Monad⇒Kleisli C TS) using () renaming (extend to extendS)
+    _#P = λ {X} {A} f → P-elgots._# {X} {A} f
+    _#S = λ {X} {A} f → S-elgots._# {X} {A} f
   record PreElgotMonad-Morphism : Set (o ⊔ ℓ ⊔ e) where
     field
       α : NaturalTransformation TP.F TS.F
@@ -40,6 +43,7 @@ module _ (P S : PreElgotMonad) where
         → α.η X ∘ TP.η.η X ≈ TS.η.η X
       α-μ : ∀ {X}
         → α.η X ∘ TP.μ.η X ≈ TS.μ.η X ∘ TS.F.₁ (α.η X) ∘ α.η (TP.F.₀ X)
+      preserves : ∀ {X A} (f : X ⇒ TP.F.₀ A + X) → α.η A ∘ f #P ≈ ((α.η A +₁ idC) ∘ f) #S
 
 PreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
 PreElgotMonads = record
@@ -57,6 +61,7 @@ PreElgotMonads = record
                    ; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
                    }
                    where
+                     open Elgot-Algebra-on using (#-resp-≈)
                      id' : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism A A
                      id' {A} = record
                        { α = ntHelper (record
@@ -68,10 +73,16 @@ PreElgotMonads = record
                          T.μ.η _ ∘ T.F.₁ idC ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
                          T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩
                          T.μ.η _ ≈⟨ sym identityˡ ⟩
-                         idC ∘ T.μ.η _ ∎) }
+                         idC ∘ T.μ.η _ ∎)
+                       ; preserves = λ f → begin
+                         idC ∘ f # ≈⟨ identityˡ ⟩
+                         f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩
+                         ((idC +₁ idC) ∘ f) # ∎
+                       }
                        where
-                         open PreElgotMonad A using (T)
+                         open PreElgotMonad A using (T; elgotalgebras)
                          module T = Monad T
+                         _# = λ {X} {A} f → elgotalgebras._# {X} {A} f
                      _∘'_ : ∀ {X Y Z : PreElgotMonad} → PreElgotMonad-Morphism Y Z → PreElgotMonad-Morphism X Y → PreElgotMonad-Morphism X Z
                      _∘'_ {X} {Y} {Z} f g = record
                         { α = αf ∘ᵥ αg
@@ -80,19 +91,27 @@ PreElgotMonads = record
                           αf.η A ∘ TY.η.η A ≈⟨ α-η f ⟩
                           TZ.η.η A ∎
                         ; α-μ = λ {A} → begin
-                           (αf.η A ∘ αg.η A) ∘ TX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩
+                          (αf.η A ∘ αg.η A) ∘ TX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩
                           αf.η A ∘ TY.μ.η A ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩
                           (TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ αf.η (TY.F.₀ A)) ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
                           TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ (TZ.F.₁ (αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism TZ.F))) ⟩
                           TZ.μ.η A ∘ (TZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩
                           TZ.μ.η A ∘ TZ.F.₁ ((αf.η A ∘ αg.η A)) ∘  αf.η (TX.F.₀ A) ∘ αg.η (TX.F.₀ A) ∎
+                        ; preserves = λ {A} {B} h → begin
+                          (αf.η B ∘ αg.η B) ∘ (h #X) ≈⟨ pullʳ (preserves g h) ⟩
+                          αf.η B ∘ ((αg.η B +₁ idC) ∘ h) #Y ≈⟨ preserves f ((αg.η B +₁ idC) ∘ h) ⟩
+                          (((αf.η B +₁ idC) ∘ (αg.η B +₁ idC) ∘ h) #Z) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
+                          (((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎
                         }
                         where
                           module TX = Monad (PreElgotMonad.T X)
                           module TY = Monad (PreElgotMonad.T Y)
                           module TZ = Monad (PreElgotMonad.T Z)
+                          _#X = λ {A} {B} f → PreElgotMonad.elgotalgebras._# X {A} {B} f
+                          _#Y = λ {A} {B} f → PreElgotMonad.elgotalgebras._# Y {A} {B} f
+                          _#Z = λ {A} {B} f → PreElgotMonad.elgotalgebras._# Z {A} {B} f
 
-                          open PreElgotMonad-Morphism using (α-η; α-μ)
+                          open PreElgotMonad-Morphism using (α-η; α-μ; preserves)
 
                           open PreElgotMonad-Morphism f using () renaming (α to αf)
                           open PreElgotMonad-Morphism g using () renaming (α to αg)

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

@@ -2,6 +2,11 @@
 ```agda
 open import Level
 open import Category.Instance.AmbientCategory
+open import Categories.FreeObjects.Free
+open import Categories.Object.Initial
+open import Categories.NaturalTransformation
+open import Categories.NaturalTransformation.Equivalence
+open import Categories.Monad
 import Monad.Instance.K as MIK
 ```
 -->
@@ -17,7 +22,8 @@ open import Monad.ElgotMonad ambient
 open import Monad.Instance.K ambient
 open import Monad.Instance.K.Compositionality ambient MK
 open import Monad.Instance.K.Commutative ambient MK
-open import Categories.FreeObjects.Free
+open import Category.Construction.PreElgotMonads ambient
+open import Category.Construction.ElgotAlgebras ambient
 
 open Equiv
 open HomReasoning
@@ -43,4 +49,36 @@ preElgot : PreElgotMonad
 preElgot = record { T = monadK ; isPreElgot = isPreElgot }
 
 -- initialPreElgot :
+initialPreElgot : IsInitial PreElgotMonads preElgot
+initialPreElgot = record
+  { ! = !′
+  ; !-unique = !-unique′
+  }
+  where
+    !′ : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism preElgot A
+    !′ {A} = record
+      { α = ntHelper (record
+        { η = η'
+        ; commute = {!!}
+        })
+      ; α-η = {!!}
+      ; α-μ = {!!}
+      }
+      where
+        open PreElgotMonad A using (T)
+        module T = Monad T
+        open PreElgotMonad preElgot using ()
+        η' : ∀ (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))
+          where open FreeObject (freeElgot X)
+    !-unique′ : ∀ {A : PreElgotMonad} (f : PreElgotMonad-Morphism preElgot A) → PreElgotMonad-Morphism.α !′ ≃ PreElgotMonad-Morphism.α f
+    !-unique′ {A} f {X} = sym (*-uniq (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)
 ```