------------------------------------------------------------------------
-- 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  = _$′_
  }