module Chapter6.IDesc.FreeMonad.IMonad where

open import Level
open import Function

open import Chapter2.Logic

record RawIMonad {k}{ℓ}{I : Set k} (M : (I → Set ℓ) → (I → Set ℓ)) :
                 Set ((suc ℓ) ⊔ k) where
  infixl  _>>=_ 
  infixr  _=<<_

  field
    return : ∀ {A} → {i : I} → A i → M A i
    _>>=_  : ∀ {A B i} → M A i → ({i : I} → A i → M B i) → M B i

  _=<<_ : ∀ {i A B} → ({i : I} → A i → M B i) → M A i → M B i
  f =<< c = c >>= f

  join : ∀ {i A} → M (M A) i → M A i
  join m = m >>= id