```------------------------------------------------------------------------
-- The Agda standard library
--
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

{-# OPTIONS --without-K --safe #-}

open import Category.Applicative.Indexed
open import Function
open import Level

record RawIMonad {i f} {I : Set i} (M : IFun I f) :
Set (i ⊔ suc f) where
infixl 1 _>>=_ _>>_ _>=>_
infixr 1 _=<<_ _<=<_

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

_>>_ : ∀ {i j k A B} → M i j A → M j k B → M i k B
m₁ >> m₂ = m₁ >>= λ _ → m₂

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

_>=>_ : ∀ {i j k a} {A : Set a} {B C} →
(A → M i j B) → (B → M j k C) → (A → M i k C)
f >=> g = _=<<_ g ∘ f

_<=<_ : ∀ {i j k B C a} {A : Set a} →
(B → M j k C) → (A → M i j B) → (A → M i k C)
g <=< f = f >=> g

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

rawIApplicative : RawIApplicative M
rawIApplicative = record
{ pure = return
; _⊛_  = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
}

open RawIApplicative rawIApplicative public

RawIMonadT : ∀ {i f} {I : Set i} (T : IFun I f → IFun I f) → Set (i ⊔ suc f)

record RawIMonadZero {i f} {I : Set i} (M : IFun I f) :
Set (i ⊔ suc f) where
field
applicativeZero : RawIApplicativeZero M

open RawIApplicativeZero applicativeZero using (∅) public

record RawIMonadPlus {i f} {I : Set i} (M : IFun I f) :
Set (i ⊔ suc f) where
field