(Strong) Pre-Elgot monads

module Monad.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
  open Ambient ambient
  open HomReasoning
  open MR C
  open Equiv
  open import Algebra.Elgot cocartesian

A monad T is a pre-Elgot monad if every TX admits an Elgot algebra structure

  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

A strong monad T is a strong pre-Elgot monad if it is a pre-Elgot monad and strength is iteration preserving

  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