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 1 _>>=_ infixr 1 _=<<_ 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