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)
open import Monad.Helper

import Categories.Morphism.Reasoning as MR

-- Every strong Elgot monad is strong pre-Elgot

module Monad.StrongElgot.StrongPreElgot {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  -- TODO