From f2b1a36a7578d3847ab904e0b76656a1300fbc24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 28 Feb 2018 19:03:11 +0100
Subject: [PATCH] Define and use `Endofunctor`

---
 src/Cat/Category/Functor.agda | 3 +++
 src/Cat/Category/Monad.agda   | 6 +++---
 2 files changed, 6 insertions(+), 3 deletions(-)

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