open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Monad.Construction.Kleisli
open import Categories.Monad hiding (id)
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor hiding (id)

module Monad.PreElgot {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  open Category C
  open Cocartesian cocartesian
  open import Algebra.Elgot cocartesian

  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 +₁ id) ∘ f) ≈ extend h ∘ elgotalgebras._# {X} f
  
  record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      T : Monad C
      isPreElgot : IsPreElgot T

    open IsPreElgot isPreElgot public