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

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

    module Function.Identity.Effectful where

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

    private
      variable
        ℓ : Level

    Identity : (A : Set ℓ) → Set ℓ
    Identity A = A

    functor : RawFunctor {ℓ} Identity
    functor = record
      { _<$>_ = id
      }

    applicative : RawApplicative {ℓ} Identity
    applicative = record
      { rawFunctor = functor
      ; pure = id
      ; _<*>_  = _$′_
      }

    monad : RawMonad {ℓ} Identity
    monad = record
      { rawApplicative = applicative
      ; _>>=_  = _|>′_
      }

    comonad : RawComonad {ℓ} Identity
    comonad = record
      { extract = id
      ; extend  = _$′_
      }