------------------------------------------------------------------------
-- The Agda standard library
--
-- The identity monad
------------------------------------------------------------------------

module Category.Monad.Identity where

open import Category.Monad

Identity : ∀ {f} → Set f → Set f
Identity A = A

IdentityMonad : ∀ {f} → RawMonad (Identity {f})
IdentityMonad = record
  { return = λ x → x
  ; _>>=_  = λ x f → f x
  }