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.StrongPreElgot {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
  open Category C
  open import Category.Distributive.Helper distributive
  open Bundles
  open import Monad.PreElgot cocartesian
  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) ∘ (id ⁂ elgotalgebras._# f) ≈ elgotalgebras._# ((strengthen.η (X , Y) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ f))
  
  record StrongPreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      SM : StrongMonad monoidal
      isStrongPreElgot : IsStrongPreElgot SM
    
    open IsStrongPreElgot isStrongPreElgot public