Working on ElgotMonad

ElgotAlgebra.agda

@@ -45,14 +45,11 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
           → f ≈ g 
           → (f #) ≈ (g #)
 
+
   --*
   -- (unguarded) Elgot-Algebra
   --*
-  record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
-    -- Object
-    field
-      A : Obj
-
+  record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
     -- iteration operator
     field
       _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A)
@@ -116,6 +113,11 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
     -- every elgot-algebra comes with a divergence constant
     !ₑ : ⊥ ⇒ A
     !ₑ = i₂ #
+  record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
+    field
+      A : Obj
+      algebra : Elgot-Algebra-on A
+    open Elgot-Algebra-on algebra public
 
   --*
   -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras
@@ -147,6 +149,8 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
   -- constructing an unguarded Elgot-Algebra from an Id-Guarded one 
   Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra
   Id-Guarded→Unguarded gea = record 
+    { A = A 
+    ; algebra = record
       { _# = _#
       ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (∘-resp-≈ˡ ([]-congˡ identityˡ))
       ; #-Uniformity = #-Uniformity
@@ -157,6 +161,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
       ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #)                                              ∎
       ; #-resp-≈ = #-resp-≈
       }
+    }
     where 
     open Guarded-Elgot-Algebra gea
     open HomReasoning

Monad/ElgotMonad.agda

@@ -0,0 +1,95 @@
+open import Level
+open import Categories.Category.Core
+open import Categories.Category.Extensive.Bundle
+open import Categories.Category.BinaryProducts
+open import Categories.Category.Cocartesian
+open import Categories.Category.Cartesian
+open import Categories.Category.Extensive
+open import ElgotAlgebra
+
+import Categories.Morphism.Reasoning as MR
+
+module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+  open HomReasoning
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
+  open BinaryProducts products hiding (η)
+  open MR C
+  open Equiv
+  
+  open import Categories.Monad
+  open import Categories.Functor
+
+  record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
+    open Monad T
+    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 ED (T₀ X)
+
+    module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
+
+    -- with the following associativity
+    field
+      assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
+  
+  record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      T : Monad C
+      isPreElgot : IsPreElgot T
+
+    open IsPreElgot isPreElgot public
+
+  record IsElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
+    open Monad T
+    open Functor F renaming (F₀ to T₀; F₁ to T₁)
+
+    -- iteration operator
+    field
+      _† : ∀ {X Y} → X ⇒ T₀ (Y + X) → X ⇒ T₀ Y
+
+    -- laws
+    field
+      Fixpoint : ∀ {X Y} {f : X ⇒ T₀ (Y + X)} → f † ≈ (μ.η _ ∘ T₁ [ η.η _ , f † ]) ∘ f
+      Naturality : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Y ⇒ T₀ Z} → (μ.η _ ∘ T₁ g) ∘ f † ≈ ((μ.η _ ∘ T₁ [ (T₁ i₁) ∘ g , η.η _ ∘ i₂ ]) ∘ f)†
+      Codiagonal : ∀ {X Y} {f : X ⇒ T₀ ((Y + X) + X)} → (T₁ [ idC , i₂ ] ∘ f )† ≈ f † †
+      Uniformity : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Z ⇒ T₀ (Y + Z)} {h : Z ⇒ X} → f ∘ h ≈ (T₁ (idC +₁ h)) ∘ g → f † ∘ h ≈ g †
+
+  record ElgotMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      T : Monad C
+      isElgot : IsElgot T
+
+    open IsElgot isElgot public
+
+  -- elgot monads are pre-elgot
+  Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
+  Elgot⇒PreElgot EM = record 
+    { T = T 
+    ; isPreElgot = record 
+      { elgotalgebras = λ {X} → record
+        { _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †
+        ; #-Fixpoint = λ {Y} {f} → begin 
+          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ Fixpoint ⟩ 
+          (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) ≈⟨ pullˡ ∘[] ⟩
+          [ (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ T₁ i₁ 
+          , (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ η.η _ ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (pullʳ (sym homomorphism)) (pullˡ (pullʳ (η.sym-commute [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]))) ⟩∘⟨refl ⟩
+          [ μ.η _ ∘ T₁ ([ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘  i₁) 
+          , (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩
+          [ μ.η _ ∘ (T₁ (η.η _))
+          , μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩
+          [ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ∎
+        ; #-Uniformity = {!   !}
+        ; #-Folding = {!   !}
+        ; #-resp-≈ = {!   !}
+        } 
+      ; assoc = {!   !} 
+      } 
+    }
+    where
+      open ElgotMonad EM
+      module T = Monad T
+      open T
+      open Functor F renaming (F₀ to T₀; F₁ to T₁)