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.Strong
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Functor hiding (id)
open import Data.Product using (_,_)
open import Categories.Category.Distributive


module Monad.StrongElgot {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
  open Category C
  open import Category.Distributive.Helper distributive
  open Bundles
  open import Monad.Elgot cocartesian
  record IsStrongElgot (SM : StrongMonad monoidal) : Set (o ⊔ ℓ ⊔ e) where
    open StrongMonad SM using (M; strengthen)
    open Monad M using (F)

    -- M is Elgot
    field
      elgot : IsElgot M
    
    open IsElgot elgot public

    -- -- and strength is iteration preserving
    -- field
    --   strengthen-preserves : ∀ {X Y Z} (f : Z ⇒ F.₀ Y + Z) 
    --     → strengthen.η (X , Y) ∘ (id ⁂ elgotalgebras._# f) ≈ elgotalgebras._# ((strengthen.η (X , Y) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ f))
  
  record StrongElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      SM : StrongMonad monoidal
      isStrongElgot : IsStrongElgot SM
    
    open IsStrongElgot isStrongElgot public