From 8a8dd0ab978fe3237a8e6ead146b8e2fb0bc79da Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 8 Feb 2024 19:53:05 +0100
Subject: [PATCH] Refactor the definition of monads (#1019)

This PR breaks up the definition of a monad into smaller parts.
---
 src/category-theory.lagda.md                  |   2 +
 .../monads-on-categories.lagda.md             | 225 ++++++++++-
 .../monads-on-precategories.lagda.md          | 375 +++++++++++++-----
 ...formations-functors-precategories.lagda.md |  43 +-
 .../pointed-endofunctors-categories.lagda.md  | 138 +++++++
 ...ointed-endofunctors-precategories.lagda.md | 141 +++++++
 6 files changed, 795 insertions(+), 129 deletions(-)
 create mode 100644 src/category-theory/pointed-endofunctors-categories.lagda.md
 create mode 100644 src/category-theory/pointed-endofunctors-precategories.lagda.md

diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index dbfc94047a..2fe0b19e5f 100644
--- a/src/category-theory.lagda.md
+++ b/src/category-theory.lagda.md
@@ -120,6 +120,8 @@ open import category-theory.opposite-categories public
 open import category-theory.opposite-large-precategories public
 open import category-theory.opposite-precategories public
 open import category-theory.opposite-preunivalent-categories public
+open import category-theory.pointed-endofunctors-categories public
+open import category-theory.pointed-endofunctors-precategories public
 open import category-theory.precategories public
 open import category-theory.precategory-of-elements-of-a-presheaf public
 open import category-theory.precategory-of-functors public
diff --git a/src/category-theory/monads-on-categories.lagda.md b/src/category-theory/monads-on-categories.lagda.md
index 181b7e3ba3..c09db9468b 100644
--- a/src/category-theory/monads-on-categories.lagda.md
+++ b/src/category-theory/monads-on-categories.lagda.md
@@ -8,23 +8,240 @@ module category-theory.monads-on-categories where
 
 ```agda
 open import category-theory.categories
+open import category-theory.functors-categories
 open import category-theory.monads-on-precategories
-open import category-theory.precategories
+open import category-theory.natural-transformations-functors-categories
+open import category-theory.pointed-endofunctors-categories
 
+open import foundation.dependent-pair-types
+open import foundation.identity-types
 open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
 ```
 
 </details>
 
+## Idea
+
+A {{#concept "monad" Disambiguation="on a category" Agda=monad-Category}} on a
+[category](category-theory.categories.md) `C` consists of an
+[endofunctor](category-theory.functors-categories.md) `T : C → C` together with
+two
+[natural transformations](category-theory.natural-transformations-functors-categories.md):
+`η : 1_C ⇒ T` and `μ : T² ⇒ T`, where `1_C : C → C` is the identity functor for
+`C`, and `T²` is the functor `T ∘ T : C → C`. These must satisfy the following
+{{#concept "monad laws" Disambiguation="monad on a category"}}:
+
+- **Associativity:** `μ ∘ (T • μ) = μ ∘ (μ • T)`
+- The **left unit law:** `μ ∘ (T • η) = 1_T`
+- The **right unit law:** `μ ∘ (η • T) = 1_T`.
+
+Here, `•` denotes
+[whiskering](category-theory.natural-transformations-functors-precategories.md#whiskering),
+and `1_T : T ⇒ T` denotes the identity natural transformation for `T`.
+
 ## Definitions
 
+### Multiplication structure on a pointed endofunctor on a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  (T : pointed-endofunctor-Category C)
+  where
+
+  structure-multiplication-pointed-endofunctor-Category : UU (l1 ⊔ l2)
+  structure-multiplication-pointed-endofunctor-Category =
+    structure-multiplication-pointed-endofunctor-Precategory
+      ( precategory-Category C)
+      ( T)
+```
+
+### Associativity of multiplication on a pointed endofunctor on a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  (T : pointed-endofunctor-Category C)
+  (μ : structure-multiplication-pointed-endofunctor-Category C T)
+  where
+
+  associative-mul-pointed-endofunctor-Category : UU (l1 ⊔ l2)
+  associative-mul-pointed-endofunctor-Category =
+    associative-mul-pointed-endofunctor-Precategory
+      ( precategory-Category C)
+      ( T)
+      ( μ)
+```
+
+### The left unit law on a multiplication on a pointed endofunctor
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  (T : pointed-endofunctor-Category C)
+  (μ : structure-multiplication-pointed-endofunctor-Category C T)
+  where
+
+  left-unit-law-mul-pointed-endofunctor-Category : UU (l1 ⊔ l2)
+  left-unit-law-mul-pointed-endofunctor-Category =
+    left-unit-law-mul-pointed-endofunctor-Precategory
+      ( precategory-Category C)
+      ( T)
+      ( μ)
+```
+
+### The right unit law on a multiplication on a pointed endofunctor
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  (T : pointed-endofunctor-Category C)
+  (μ : structure-multiplication-pointed-endofunctor-Category C T)
+  where
+
+  right-unit-law-mul-pointed-endofunctor-Category : UU (l1 ⊔ l2)
+  right-unit-law-mul-pointed-endofunctor-Category =
+    right-unit-law-mul-pointed-endofunctor-Precategory
+      ( precategory-Category C)
+      ( T)
+      ( μ)
+```
+
+### The structure of a monad on a pointed endofunctor on a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  (T : pointed-endofunctor-Category C)
+  where
+
+  structure-monad-pointed-endofunctor-Category : UU (l1 ⊔ l2)
+  structure-monad-pointed-endofunctor-Category =
+    structure-monad-pointed-endofunctor-Precategory
+      ( precategory-Category C)
+      ( T)
+```
+
 ### The type of monads on categories
 
 ```agda
 module _
-  {l : Level} (C : Category l l)
+  {l1 l2 : Level} (C : Category l1 l2)
   where
 
-  monad-Category : UU l
-  monad-Category = monad-Precategory l (precategory-Category C)
+  monad-Category : UU (l1 ⊔ l2)
+  monad-Category = monad-Precategory (precategory-Category C)
+
+  module _
+    (T : monad-Category)
+    where
+
+    pointed-endofunctor-monad-Category :
+      pointed-endofunctor-Category C
+    pointed-endofunctor-monad-Category =
+      pointed-endofunctor-monad-Precategory (precategory-Category C) T
+
+    endofunctor-monad-Category :
+      functor-Category C C
+    endofunctor-monad-Category =
+      endofunctor-monad-Precategory (precategory-Category C) T
+
+    obj-endofunctor-monad-Category :
+      obj-Category C → obj-Category C
+    obj-endofunctor-monad-Category =
+      obj-endofunctor-monad-Precategory (precategory-Category C) T
+
+    hom-endofunctor-monad-Category :
+      {X Y : obj-Category C} →
+      hom-Category C X Y →
+      hom-Category C
+        ( obj-endofunctor-monad-Category X)
+        ( obj-endofunctor-monad-Category Y)
+    hom-endofunctor-monad-Category =
+      hom-endofunctor-monad-Precategory (precategory-Category C) T
+
+    preserves-id-endofunctor-monad-Category :
+      (X : obj-Category C) →
+      hom-endofunctor-monad-Category (id-hom-Category C {X}) ＝
+      id-hom-Category C
+    preserves-id-endofunctor-monad-Category =
+      preserves-id-endofunctor-monad-Precategory (precategory-Category C) T
+
+    preserves-comp-endofunctor-monad-Category :
+      {X Y Z : obj-Category C} →
+      (g : hom-Category C Y Z) (f : hom-Category C X Y) →
+      hom-endofunctor-monad-Category (comp-hom-Category C g f) ＝
+      comp-hom-Category C
+        ( hom-endofunctor-monad-Category g)
+        ( hom-endofunctor-monad-Category f)
+    preserves-comp-endofunctor-monad-Category =
+      preserves-comp-endofunctor-monad-Precategory (precategory-Category C) T
+
+    unit-monad-Category :
+      pointing-endofunctor-Category C endofunctor-monad-Category
+    unit-monad-Category =
+      unit-monad-Precategory (precategory-Category C) T
+
+    hom-unit-monad-Category :
+      hom-family-functor-Category C C
+        ( id-functor-Category C)
+        ( endofunctor-monad-Category)
+    hom-unit-monad-Category =
+      hom-unit-monad-Precategory (precategory-Category C) T
+
+    naturality-unit-monad-Category :
+      is-natural-transformation-Category C C
+        ( id-functor-Category C)
+        ( endofunctor-monad-Category)
+        ( hom-unit-monad-Category)
+    naturality-unit-monad-Category =
+      naturality-unit-monad-Precategory (precategory-Category C) T
+
+    mul-monad-Category :
+      structure-multiplication-pointed-endofunctor-Category C
+        ( pointed-endofunctor-monad-Category)
+    mul-monad-Category =
+      mul-monad-Precategory (precategory-Category C) T
+
+    hom-mul-monad-Category :
+      hom-family-functor-Category C C
+        ( comp-functor-Category C C C
+          ( endofunctor-monad-Category)
+          ( endofunctor-monad-Category))
+        ( endofunctor-monad-Category)
+    hom-mul-monad-Category =
+      hom-mul-monad-Precategory (precategory-Category C) T
+
+    naturality-mul-monad-Category :
+      is-natural-transformation-Category C C
+        ( comp-functor-Category C C C
+          ( endofunctor-monad-Category)
+          ( endofunctor-monad-Category))
+        ( endofunctor-monad-Category)
+        ( hom-mul-monad-Category)
+    naturality-mul-monad-Category =
+      naturality-mul-monad-Precategory (precategory-Category C) T
+
+    associative-mul-monad-Category :
+      associative-mul-pointed-endofunctor-Category C
+        ( pointed-endofunctor-monad-Category)
+        ( mul-monad-Category)
+    associative-mul-monad-Category =
+      associative-mul-monad-Precategory (precategory-Category C) T
+
+    left-unit-law-mul-monad-Category :
+      left-unit-law-mul-pointed-endofunctor-Category C
+        ( pointed-endofunctor-monad-Category)
+        ( mul-monad-Category)
+    left-unit-law-mul-monad-Category =
+      left-unit-law-mul-monad-Precategory (precategory-Category C) T
+
+    right-unit-law-mul-monad-Category :
+      right-unit-law-mul-pointed-endofunctor-Category C
+        ( pointed-endofunctor-monad-Category)
+        ( mul-monad-Category)
+    right-unit-law-mul-monad-Category =
+      right-unit-law-mul-monad-Precategory (precategory-Category C) T
 ```
diff --git a/src/category-theory/monads-on-precategories.lagda.md b/src/category-theory/monads-on-precategories.lagda.md
index 57719359e6..63225d5d66 100644
--- a/src/category-theory/monads-on-precategories.lagda.md
+++ b/src/category-theory/monads-on-precategories.lagda.md
@@ -9,6 +9,7 @@ module category-theory.monads-on-precategories where
 ```agda
 open import category-theory.functors-precategories
 open import category-theory.natural-transformations-functors-precategories
+open import category-theory.pointed-endofunctors-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
@@ -22,17 +23,18 @@ open import foundation-core.cartesian-product-types
 
 ## Idea
 
-A monad on a precategory `C` consists of an
-endo[functor](category-theory.functors-precategories.md) `T : C → C` together
+A {{#concept "monad" Disambiguation="on a precategory" Agda=monad-Precategory}}
+on a [precategory](category-theory.precategories.md) `C` consists of an
+[endofunctor](category-theory.functors-precategories.md) `T : C → C` together
 with two
 [natural transformations](category-theory.natural-transformations-functors-precategories.md):
-`η : 1_C ⇒ T` and `μ : T² ⇒ T` (where `1_C : C → C` is the identity functor for
-`C`, and `T²` is the functor `T ∘ T : C → C`).
+`η : 1_C ⇒ T` and `μ : T² ⇒ T`, where `1_C : C → C` is the identity functor for
+`C`, and `T²` is the functor `T ∘ T : C → C`. These must satisfy the following
+{{#concept "monad laws" Disambiguation="monad on a precategory"}}:
 
-These must fulfill the _coherence conditions_:
-
-- `μ ∘ (T • μ) = μ ∘ (μ • T)`, and
-- `μ ∘ (T • η) = μ ∘ (η • T) = 1_T`.
+- **Associativity:** `μ ∘ (T • μ) = μ ∘ (μ • T)`
+- The **left unit law:** `μ ∘ (T • η) = 1_T`
+- The **right unit law:** `μ ∘ (η • T) = 1_T`.
 
 Here, `•` denotes
 [whiskering](category-theory.natural-transformations-functors-precategories.md#whiskering),
@@ -40,95 +42,276 @@ and `1_T : T ⇒ T` denotes the identity natural transformation for `T`.
 
 ## Definitions
 
+### Multiplication structure on a pointed endofunctor on a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  (T : pointed-endofunctor-Precategory C)
+  where
+
+  structure-multiplication-pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
+  structure-multiplication-pointed-endofunctor-Precategory =
+    natural-transformation-Precategory C C
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T))
+      ( functor-pointed-endofunctor-Precategory C T)
+```
+
+### Associativity of multiplication on a pointed endofunctor on a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  (T : pointed-endofunctor-Precategory C)
+  (μ : structure-multiplication-pointed-endofunctor-Precategory C T)
+  where
+
+  associative-mul-pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
+  associative-mul-pointed-endofunctor-Precategory =
+    comp-natural-transformation-Precategory C C
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( comp-functor-Precategory C C C
+          ( functor-pointed-endofunctor-Precategory C T)
+          ( functor-pointed-endofunctor-Precategory C T)))
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T))
+      ( functor-pointed-endofunctor-Precategory C T)
+      ( μ)
+      ( left-whisker-natural-transformation-Precategory C C C
+        ( comp-functor-Precategory C C C
+          ( functor-pointed-endofunctor-Precategory C T)
+          ( functor-pointed-endofunctor-Precategory C T))
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( μ)) ＝
+    comp-natural-transformation-Precategory C C
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( comp-functor-Precategory C C C
+          ( functor-pointed-endofunctor-Precategory C T)
+          ( functor-pointed-endofunctor-Precategory C T)))
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T))
+      ( functor-pointed-endofunctor-Precategory C T)
+      ( μ)
+      ( right-whisker-natural-transformation-Precategory C C C
+        ( comp-functor-Precategory C C C
+          ( functor-pointed-endofunctor-Precategory C T)
+          ( functor-pointed-endofunctor-Precategory C T))
+          ( functor-pointed-endofunctor-Precategory C T)
+          ( μ)
+          ( functor-pointed-endofunctor-Precategory C T))
+```
+
+### The left unit law on a multiplication on a pointed endofunctor
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  (T : pointed-endofunctor-Precategory C)
+  (μ : structure-multiplication-pointed-endofunctor-Precategory C T)
+  where
+
+  left-unit-law-mul-pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
+  left-unit-law-mul-pointed-endofunctor-Precategory =
+    comp-natural-transformation-Precategory C C
+      ( functor-pointed-endofunctor-Precategory C T)
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T))
+      ( functor-pointed-endofunctor-Precategory C T)
+      ( μ)
+      ( left-whisker-natural-transformation-Precategory C C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( pointing-pointed-endofunctor-Precategory C T)) ＝
+    id-natural-transformation-Precategory C C
+      ( functor-pointed-endofunctor-Precategory C T)
+```
+
+### The right unit law on a multiplication on a pointed endofunctor
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  (T : pointed-endofunctor-Precategory C)
+  (μ : structure-multiplication-pointed-endofunctor-Precategory C T)
+  where
+
+  right-unit-law-mul-pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
+  right-unit-law-mul-pointed-endofunctor-Precategory =
+    comp-natural-transformation-Precategory C C
+      ( functor-pointed-endofunctor-Precategory C T)
+      ( comp-functor-Precategory C C C
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T))
+      ( functor-pointed-endofunctor-Precategory C T)
+      ( μ)
+      ( right-whisker-natural-transformation-Precategory C C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory C T)
+        ( pointing-pointed-endofunctor-Precategory C T)
+        ( functor-pointed-endofunctor-Precategory C T)) ＝
+    id-natural-transformation-Precategory C C
+      ( functor-pointed-endofunctor-Precategory C T)
+```
+
+### The structure of a monad on a pointed endofunctor on a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  (T : pointed-endofunctor-Precategory C)
+  where
+
+  structure-monad-pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
+  structure-monad-pointed-endofunctor-Precategory =
+    Σ ( structure-multiplication-pointed-endofunctor-Precategory C T)
+      ( λ μ →
+        associative-mul-pointed-endofunctor-Precategory C T μ ×
+        left-unit-law-mul-pointed-endofunctor-Precategory C T μ ×
+        right-unit-law-mul-pointed-endofunctor-Precategory C T μ)
+```
+
 ### The type of monads on precategories
 
 ```agda
-monad-Precategory :
-  (l : Level) (C : Precategory l l) → UU l
-monad-Precategory l C =
-  Σ ( functor-Precategory C C)
-    ( λ T →
-      Σ ( natural-transformation-Precategory C C (id-functor-Precategory C) T)
-        ( λ eta →
-          Σ ( natural-transformation-Precategory
-              ( C)
-              ( C)
-              ( comp-functor-Precategory C C C T T) T)
-            ( λ mu →
-              Σ ( comp-natural-transformation-Precategory
-                    ( C)
-                    ( C)
-                    ( comp-functor-Precategory
-                      ( C)
-                      ( C)
-                      ( C)
-                      ( T)
-                      ( comp-functor-Precategory C C C T T))
-                    ( comp-functor-Precategory C C C T T)
-                    ( T)
-                    ( mu)
-                    ( whiskering-functor-natural-transformation-Precategory
-                      {C = C}
-                      {D = C}
-                      {E = C}
-                      ( comp-functor-Precategory C C C T T)
-                      ( T)
-                      ( T)
-                      ( mu))
-                  ＝
-                    comp-natural-transformation-Precategory
-                      ( C)
-                      ( C)
-                      (comp-functor-Precategory
-                        ( C)
-                        ( C)
-                        ( C)
-                        ( comp-functor-Precategory C C C T T) T)
-                      ( comp-functor-Precategory C C C T T)
-                      ( T)
-                      ( mu)
-                      ( whiskering-natural-transformation-functor-Precategory
-                        {C = C}
-                        {D = C}
-                        {E = C}
-                        ( comp-functor-Precategory C C C T T)
-                        ( T)
-                        ( mu)
-                        ( T)))
-                  ( λ _ →
-                    product
-                      ( comp-natural-transformation-Precategory
-                          ( C)
-                          ( C)
-                          ( T)
-                          ( comp-functor-Precategory C C C T T)
-                          ( T)
-                          ( mu)
-                          ( whiskering-functor-natural-transformation-Precategory
-                            {C = C}
-                            {D = C}
-                            {E = C}
-                            ( id-functor-Precategory C)
-                            ( T)
-                            ( T)
-                            ( eta))
-                      ＝
-                        id-natural-transformation-Precategory C C T)
-                      ( comp-natural-transformation-Precategory
-                          ( C)
-                          ( C)
-                          ( T)
-                          ( comp-functor-Precategory C C C T T)
-                          ( T)
-                          ( mu)
-                          ( whiskering-natural-transformation-functor-Precategory
-                            {C = C}
-                            {D = C}
-                            {E = C}
-                            ( id-functor-Precategory C)
-                            ( T)
-                            ( eta)
-                            ( T))
-                      ＝
-                        id-natural-transformation-Precategory C C T)))))
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  monad-Precategory : UU (l1 ⊔ l2)
+  monad-Precategory =
+    Σ ( pointed-endofunctor-Precategory C)
+      ( structure-monad-pointed-endofunctor-Precategory C)
+
+  module _
+    (T : monad-Precategory)
+    where
+
+    pointed-endofunctor-monad-Precategory :
+      pointed-endofunctor-Precategory C
+    pointed-endofunctor-monad-Precategory = pr1 T
+
+    endofunctor-monad-Precategory :
+      functor-Precategory C C
+    endofunctor-monad-Precategory =
+      functor-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+
+    obj-endofunctor-monad-Precategory :
+      obj-Precategory C → obj-Precategory C
+    obj-endofunctor-monad-Precategory =
+      obj-functor-Precategory C C endofunctor-monad-Precategory
+
+    hom-endofunctor-monad-Precategory :
+      {X Y : obj-Precategory C} →
+      hom-Precategory C X Y →
+      hom-Precategory C
+        ( obj-endofunctor-monad-Precategory X)
+        ( obj-endofunctor-monad-Precategory Y)
+    hom-endofunctor-monad-Precategory =
+      hom-functor-Precategory C C endofunctor-monad-Precategory
+
+    preserves-id-endofunctor-monad-Precategory :
+      (X : obj-Precategory C) →
+      hom-endofunctor-monad-Precategory (id-hom-Precategory C {X}) ＝
+      id-hom-Precategory C
+    preserves-id-endofunctor-monad-Precategory =
+      preserves-id-functor-Precategory C C endofunctor-monad-Precategory
+
+    preserves-comp-endofunctor-monad-Precategory :
+      {X Y Z : obj-Precategory C} →
+      (g : hom-Precategory C Y Z) (f : hom-Precategory C X Y) →
+      hom-endofunctor-monad-Precategory (comp-hom-Precategory C g f) ＝
+      comp-hom-Precategory C
+        ( hom-endofunctor-monad-Precategory g)
+        ( hom-endofunctor-monad-Precategory f)
+    preserves-comp-endofunctor-monad-Precategory =
+      preserves-comp-functor-Precategory C C
+        ( endofunctor-monad-Precategory)
+
+    unit-monad-Precategory :
+      pointing-endofunctor-Precategory C endofunctor-monad-Precategory
+    unit-monad-Precategory =
+      pointing-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+
+    hom-unit-monad-Precategory :
+      hom-family-functor-Precategory C C
+        ( id-functor-Precategory C)
+        ( endofunctor-monad-Precategory)
+    hom-unit-monad-Precategory =
+      hom-family-pointing-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+
+    naturality-unit-monad-Precategory :
+      is-natural-transformation-Precategory C C
+        ( id-functor-Precategory C)
+        ( endofunctor-monad-Precategory)
+        ( hom-unit-monad-Precategory)
+    naturality-unit-monad-Precategory =
+      naturality-pointing-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+
+    mul-monad-Precategory :
+      structure-multiplication-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+    mul-monad-Precategory = pr1 (pr2 T)
+
+    hom-mul-monad-Precategory :
+      hom-family-functor-Precategory C C
+        ( comp-functor-Precategory C C C
+          ( endofunctor-monad-Precategory)
+          ( endofunctor-monad-Precategory))
+        ( endofunctor-monad-Precategory)
+    hom-mul-monad-Precategory =
+      hom-family-natural-transformation-Precategory C C
+        ( comp-functor-Precategory C C C
+          ( endofunctor-monad-Precategory)
+          ( endofunctor-monad-Precategory))
+        ( endofunctor-monad-Precategory)
+        ( mul-monad-Precategory)
+
+    naturality-mul-monad-Precategory :
+      is-natural-transformation-Precategory C C
+        ( comp-functor-Precategory C C C
+          ( endofunctor-monad-Precategory)
+          ( endofunctor-monad-Precategory))
+        ( endofunctor-monad-Precategory)
+        ( hom-mul-monad-Precategory)
+    naturality-mul-monad-Precategory =
+      naturality-natural-transformation-Precategory C C
+        ( comp-functor-Precategory C C C
+          ( endofunctor-monad-Precategory)
+          ( endofunctor-monad-Precategory))
+        ( endofunctor-monad-Precategory)
+        ( mul-monad-Precategory)
+
+    associative-mul-monad-Precategory :
+      associative-mul-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+        ( mul-monad-Precategory)
+    associative-mul-monad-Precategory =
+      pr1 (pr2 (pr2 T))
+
+    left-unit-law-mul-monad-Precategory :
+      left-unit-law-mul-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+        ( mul-monad-Precategory)
+    left-unit-law-mul-monad-Precategory =
+      pr1 (pr2 (pr2 (pr2 T)))
+
+    right-unit-law-mul-monad-Precategory :
+      right-unit-law-mul-pointed-endofunctor-Precategory C
+        ( pointed-endofunctor-monad-Precategory)
+        ( mul-monad-Precategory)
+    right-unit-law-mul-monad-Precategory =
+      pr2 (pr2 (pr2 (pr2 T)))
 ```
diff --git a/src/category-theory/natural-transformations-functors-precategories.lagda.md b/src/category-theory/natural-transformations-functors-precategories.lagda.md
index db1057f147..2bb9c36a2c 100644
--- a/src/category-theory/natural-transformations-functors-precategories.lagda.md
+++ b/src/category-theory/natural-transformations-functors-precategories.lagda.md
@@ -277,12 +277,12 @@ transformation.
 ```agda
 module _
   {l1 l2 l3 l4 l5 l6 : Level}
-  {C : Precategory l1 l2}
-  {D : Precategory l3 l4}
-  {E : Precategory l5 l6}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (E : Precategory l5 l6)
   where
 
-  whiskering-functor-natural-transformation-Precategory :
+  left-whisker-natural-transformation-Precategory :
     (F G : functor-Precategory C D)
     (H : functor-Precategory D E)
     (α : natural-transformation-Precategory C D F G) →
@@ -291,7 +291,7 @@ module _
       ( E)
       ( comp-functor-Precategory C D E H F)
       ( comp-functor-Precategory C D E H G)
-  whiskering-functor-natural-transformation-Precategory F G H α =
+  left-whisker-natural-transformation-Precategory F G H α =
     ( λ x → (pr1 (pr2 H)) ((pr1 α) x)) ,
     ( λ {x} {y} → λ f →
       inv
@@ -309,7 +309,7 @@ module _
         ( (pr1 α) y)
         ( (pr1 (pr2 F)) f)))
 
-  whiskering-natural-transformation-functor-Precategory :
+  right-whisker-natural-transformation-Precategory :
     (F G : functor-Precategory C D)
     (α : natural-transformation-Precategory C D F G)
     (K : functor-Precategory E C) →
@@ -318,7 +318,7 @@ module _
       ( D)
       ( comp-functor-Precategory E C D F K)
       ( comp-functor-Precategory E C D G K)
-  whiskering-natural-transformation-functor-Precategory F G α K =
+  right-whisker-natural-transformation-Precategory F G α K =
     (λ x → (pr1 α) ((pr1 K) x)) , (λ f → (pr2 α) ((pr1 (pr2 K)) f))
 ```
 
@@ -336,10 +336,11 @@ transformations obtained by whiskering.
 ```agda
 module _
   {l1 l2 l3 l4 l5 l6 : Level}
-  {C : Precategory l1 l2}
-  {D : Precategory l3 l4}
-  {E : Precategory l5 l6}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (E : Precategory l5 l6)
   where
+
   horizontal-comp-natural-transformation-Precategory :
     (F G : functor-Precategory C D)
     (H I : functor-Precategory D E)
@@ -351,26 +352,10 @@ module _
       ( comp-functor-Precategory C D E H F)
       ( comp-functor-Precategory C D E I G)
   horizontal-comp-natural-transformation-Precategory F G H I β α =
-    comp-natural-transformation-Precategory
-      ( C)
-      ( E)
+    comp-natural-transformation-Precategory C E
       ( comp-functor-Precategory C D E H F)
       ( comp-functor-Precategory C D E H G)
       ( comp-functor-Precategory C D E I G)
-      ( whiskering-natural-transformation-functor-Precategory
-        {C = D}
-        {D = E}
-        {E = C}
-        ( H)
-        ( I)
-        ( β)
-        ( G))
-      ( whiskering-functor-natural-transformation-Precategory
-        {C = C}
-        {D = D}
-        {E = E}
-        ( F)
-        ( G)
-        ( H)
-        ( α))
+      ( right-whisker-natural-transformation-Precategory D E C H I β G)
+      ( left-whisker-natural-transformation-Precategory C D E F G H α)
 ```
diff --git a/src/category-theory/pointed-endofunctors-categories.lagda.md b/src/category-theory/pointed-endofunctors-categories.lagda.md
new file mode 100644
index 0000000000..f5d7468bb0
--- /dev/null
+++ b/src/category-theory/pointed-endofunctors-categories.lagda.md
@@ -0,0 +1,138 @@
+# Pointed endofunctors on categories
+
+```agda
+module category-theory.pointed-endofunctors-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.functors-categories
+open import category-theory.natural-transformations-functors-categories
+open import category-theory.pointed-endofunctors-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An [endofunctor](category-theory.functors-categories.md) `F : C → C` on a
+[category](category-theory.categories.md) `C` is said to be
+{{#concept "pointed" Disambiguation="endofunctor on a category" Agda=pointed-endofunctor-Category}}
+if it comes equipped with a
+[natural transformation](category-theory.natural-transformations-functors-categories.md)
+`id ⇒ F` from the identity [functor](category-theory.functors-categories.md) to
+`F`.
+
+More explicitly, a
+{{#concept "pointing" Disambiguation="endofunctor on a category" Agda=pointing-endofunctor-Category}}
+of an endofunctor `F : C → C` consists of a family of morphisms `η X : X → F X`
+such that for each morphism `f : X → Y` in `C` the diagram
+
+```text
+       η X
+    X -----> F X
+    |         |
+  f |         | F f
+    ∨         ∨
+    Y -----> F Y
+       η Y
+```
+
+[commutes](category-theory.commuting-squares-of-morphisms-in-precategories.md).
+
+## Definitions
+
+### The structure of a pointing on an endofunctor on a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2) (T : functor-Category C C)
+  where
+
+  pointing-endofunctor-Category : UU (l1 ⊔ l2)
+  pointing-endofunctor-Category =
+    pointing-endofunctor-Precategory (precategory-Category C) T
+```
+
+### Pointed endofunctors on a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2)
+  where
+
+  pointed-endofunctor-Category : UU (l1 ⊔ l2)
+  pointed-endofunctor-Category =
+    pointed-endofunctor-Precategory (precategory-Category C)
+
+  module _
+    (F : pointed-endofunctor-Category)
+    where
+
+    functor-pointed-endofunctor-Category :
+      functor-Category C C
+    functor-pointed-endofunctor-Category =
+      functor-pointed-endofunctor-Precategory (precategory-Category C) F
+
+    obj-pointed-endofunctor-Category : obj-Category C → obj-Category C
+    obj-pointed-endofunctor-Category =
+      obj-pointed-endofunctor-Precategory (precategory-Category C) F
+
+    hom-pointed-endofunctor-Category :
+      {X Y : obj-Category C} →
+      hom-Category C X Y →
+      hom-Category C
+        ( obj-pointed-endofunctor-Category X)
+        ( obj-pointed-endofunctor-Category Y)
+    hom-pointed-endofunctor-Category =
+      hom-pointed-endofunctor-Precategory (precategory-Category C) F
+
+    preserves-id-pointed-endofunctor-Category :
+      (X : obj-Category C) →
+      hom-pointed-endofunctor-Category (id-hom-Category C {X}) ＝
+      id-hom-Category C
+    preserves-id-pointed-endofunctor-Category =
+      preserves-id-pointed-endofunctor-Precategory (precategory-Category C) F
+
+    preserves-comp-pointed-endofunctor-Category :
+      {X Y Z : obj-Category C}
+      (g : hom-Category C Y Z) (f : hom-Category C X Y) →
+      hom-pointed-endofunctor-Category
+        ( comp-hom-Category C g f) ＝
+      comp-hom-Category C
+        ( hom-pointed-endofunctor-Category g)
+        ( hom-pointed-endofunctor-Category f)
+    preserves-comp-pointed-endofunctor-Category =
+      preserves-comp-pointed-endofunctor-Precategory (precategory-Category C) F
+
+    pointing-pointed-endofunctor-Category :
+      natural-transformation-Category C C
+        ( id-functor-Category C)
+        ( functor-pointed-endofunctor-Category)
+    pointing-pointed-endofunctor-Category =
+      pointing-pointed-endofunctor-Precategory (precategory-Category C) F
+
+    hom-family-pointing-pointed-endofunctor-Category :
+      hom-family-functor-Category C C
+        ( id-functor-Category C)
+        ( functor-pointed-endofunctor-Category)
+    hom-family-pointing-pointed-endofunctor-Category =
+      hom-family-pointing-pointed-endofunctor-Precategory
+        ( precategory-Category C)
+        ( F)
+
+    naturality-pointing-pointed-endofunctor-Category :
+      is-natural-transformation-Category C C
+        ( id-functor-Category C)
+        ( functor-pointed-endofunctor-Category)
+        ( hom-family-pointing-pointed-endofunctor-Category)
+    naturality-pointing-pointed-endofunctor-Category =
+      naturality-pointing-pointed-endofunctor-Precategory
+        ( precategory-Category C) F
+```
diff --git a/src/category-theory/pointed-endofunctors-precategories.lagda.md b/src/category-theory/pointed-endofunctors-precategories.lagda.md
new file mode 100644
index 0000000000..2472a4dab6
--- /dev/null
+++ b/src/category-theory/pointed-endofunctors-precategories.lagda.md
@@ -0,0 +1,141 @@
+# Pointed endofunctors
+
+```agda
+module category-theory.pointed-endofunctors-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.functors-precategories
+open import category-theory.natural-transformations-functors-precategories
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An [endofunctor](category-theory.functors-precategories.md) `F : C → C` on a
+[precategory](category-theory.precategories.md) `C` is said to be
+{{#concept "pointed" Disambiguation="endofunctor on a category" Agda=pointed-endofunctor-Precategory}}
+if it comes equipped with a
+[natural transformation](category-theory.natural-transformations-functors-precategories.md)
+`id ⇒ F` from the identity [functor](category-theory.functors-precategories.md)
+to `F`.
+
+More explicitly, a
+{{#concept "pointing" Disambiguation="endofunctor on a precategory" Agda=pointing-endofunctor-Precategory}}
+of an endofunctor `F : C → C` consists of a family of morphisms `η X : X → F X`
+such that for each morphism `f : X → Y` in `C` the diagram
+
+```text
+       η X
+    X -----> F X
+    |         |
+  f |         | F f
+    ∨         ∨
+    Y -----> F Y
+       η Y
+```
+
+[commutes](category-theory.commuting-squares-of-morphisms-in-precategories.md).
+
+## Definitions
+
+### The structure of a pointing on an endofunctor on a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) (T : functor-Precategory C C)
+  where
+
+  pointing-endofunctor-Precategory : UU (l1 ⊔ l2)
+  pointing-endofunctor-Precategory =
+    natural-transformation-Precategory C C (id-functor-Precategory C) T
+```
+
+### Pointed endofunctors on a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
+  pointed-endofunctor-Precategory =
+    Σ (functor-Precategory C C) (pointing-endofunctor-Precategory C)
+
+  module _
+    (F : pointed-endofunctor-Precategory)
+    where
+
+    functor-pointed-endofunctor-Precategory :
+      functor-Precategory C C
+    functor-pointed-endofunctor-Precategory =
+      pr1 F
+
+    obj-pointed-endofunctor-Precategory : obj-Precategory C → obj-Precategory C
+    obj-pointed-endofunctor-Precategory =
+      obj-functor-Precategory C C functor-pointed-endofunctor-Precategory
+
+    hom-pointed-endofunctor-Precategory :
+      {X Y : obj-Precategory C} →
+      hom-Precategory C X Y →
+      hom-Precategory C
+        ( obj-pointed-endofunctor-Precategory X)
+        ( obj-pointed-endofunctor-Precategory Y)
+    hom-pointed-endofunctor-Precategory =
+      hom-functor-Precategory C C functor-pointed-endofunctor-Precategory
+
+    preserves-id-pointed-endofunctor-Precategory :
+      (X : obj-Precategory C) →
+      hom-pointed-endofunctor-Precategory (id-hom-Precategory C {X}) ＝
+      id-hom-Precategory C
+    preserves-id-pointed-endofunctor-Precategory =
+      preserves-id-functor-Precategory C C
+        ( functor-pointed-endofunctor-Precategory)
+
+    preserves-comp-pointed-endofunctor-Precategory :
+      {X Y Z : obj-Precategory C}
+      (g : hom-Precategory C Y Z) (f : hom-Precategory C X Y) →
+      hom-pointed-endofunctor-Precategory
+        ( comp-hom-Precategory C g f) ＝
+      comp-hom-Precategory C
+        ( hom-pointed-endofunctor-Precategory g)
+        ( hom-pointed-endofunctor-Precategory f)
+    preserves-comp-pointed-endofunctor-Precategory =
+      preserves-comp-functor-Precategory C C
+        ( functor-pointed-endofunctor-Precategory)
+
+    pointing-pointed-endofunctor-Precategory :
+      natural-transformation-Precategory C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory)
+    pointing-pointed-endofunctor-Precategory = pr2 F
+
+    hom-family-pointing-pointed-endofunctor-Precategory :
+      hom-family-functor-Precategory C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory)
+    hom-family-pointing-pointed-endofunctor-Precategory =
+      hom-family-natural-transformation-Precategory C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory)
+        ( pointing-pointed-endofunctor-Precategory)
+
+    naturality-pointing-pointed-endofunctor-Precategory :
+      is-natural-transformation-Precategory C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory)
+        ( hom-family-pointing-pointed-endofunctor-Precategory)
+    naturality-pointing-pointed-endofunctor-Precategory =
+      naturality-natural-transformation-Precategory C C
+        ( id-functor-Precategory C)
+        ( functor-pointed-endofunctor-Precategory)
+        ( pointing-pointed-endofunctor-Precategory)
+```