------------------------------------------------------------------------
-- 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 = _$′_
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4