diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index d648728..898a331 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -45,6 +45,9 @@ module _ {ℓc ℓc' ℓd ℓd'} open Functor +EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _ +EndoFunctor ℂ = Functor ℂ ℂ + module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 703904d..d10c5a0 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -22,7 +22,7 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where record RawMonad : Set ℓ where field -- R ~ m - R : Functor ℂ ℂ + R : EndoFunctor ℂ -- η ~ pure ηNatTrans : NaturalTransformation F.identity R -- μ ~ join @@ -208,7 +208,7 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where bind (pure ∘ g) ∘ bind (pure ∘ f) ∎ -- TODO: Naming! - R : Functor ℂ ℂ + R : EndoFunctor ℂ Functor.raw R = rawR Functor.isFunctor R = isFunctorR @@ -275,7 +275,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where open K.Monad m open NaturalTransformation ℂ ℂ - R² : Functor ℂ ℂ + R² : EndoFunctor ℂ R² = F[ R ∘ R ] ηNatTrans : NaturalTransformation F.identity R