    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An effectful view of the identity function
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Effect.Monad.Identity where

    open import Effect.Functor using (RawFunctor)
    open import Effect.Applicative using (RawApplicative)
    open import Effect.Monad using (RawMonad; module Join)
    open import Effect.Comonad using (RawComonad)
    open import Function.Base using (id; _∘′_; _|>′_; _$′_; flip)
    open import Level using (Level)

    private
      variable
        a : Level
        A : Set a

    record Identity (A : Set a) : Set a where
      constructor mkIdentity
      field runIdentity : A
    open Identity public

    functor : RawFunctor {a} Identity
    functor = record
      { _<$>_ = λ f a → mkIdentity (f (runIdentity a))
      }

    applicative : RawApplicative {a} Identity
    applicative = record
      { rawFunctor = functor
      ; pure = mkIdentity
      ; _<*>_  = λ f a → mkIdentity (runIdentity f $′ runIdentity a)
      }

    monad : RawMonad {a} Identity
    monad = record
      { rawApplicative = applicative
      ; _>>=_  = _|>′_ ∘′ runIdentity
      }

    comonad : RawComonad {a} Identity
    comonad = record
      { extract = runIdentity
      ; extend  = λ f a → mkIdentity (f a)
      }

    join : Identity (Identity A) → Identity A
    join = Join.join monad