Definition of monads on precategories and categories (+ of whiskering and horizontal composition)

src/category-theory.lagda.md

@@ -96,6 +96,8 @@ open import category-theory.maps-from-small-to-large-categories public
 open import category-theory.maps-from-small-to-large-precategories public
 open import category-theory.maps-precategories public
 open import category-theory.maps-set-magmoids public
+open import category-theory.monads-on-categories public
+open import category-theory.monads-on-precategories public
 open import category-theory.monomorphisms-in-large-precategories public
 open import category-theory.natural-isomorphisms-functors-categories public
 open import category-theory.natural-isomorphisms-functors-large-precategories public

src/category-theory/monads-on-categories.lagda.md

@@ -0,0 +1,30 @@
+# Monads on categories
+
+```agda
+module category-theory.monads-on-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.monads-on-precategories
+open import category-theory.precategories
+
+open import foundation.universe-levels
+```
+
+</details>
+
+## Definitions
+
+### The type of monads on categories
+
+```agda
+module _
+  {l : Level} (C : Category l l)
+  where
+
+  monad-Category : UU l
+  monad-Category = monad-Precategory l (precategory-Category C)
+```

src/category-theory/monads-on-precategories.lagda.md

@@ -0,0 +1,134 @@
+# Monads on precategories
+
+```agda
+module category-theory.monads-on-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
+
+open import foundation-core.cartesian-product-types
+```
+
+</details>
+
+## Idea
+
+A monad on a precategory `C` consists of an
+endo[functor](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`).
+
+These must fulfill the _coherence conditions_:
+
+- `μ ∘ (T • μ) = μ ∘ (μ • T)`, and
+- `μ ∘ (T • η) = μ ∘ (η • 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
+
+### 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)))
+                  ( λ _ →
+                    prod
+                      ( 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)))))
+```

src/category-theory/natural-transformations-functors-precategories.lagda.md

@@ -1,6 +1,8 @@
 # Natural transformations between functors between precategories
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module category-theory.natural-transformations-functors-precategories where
 ```
 
@@ -11,6 +13,7 @@ open import category-theory.functors-precategories
 open import category-theory.natural-transformations-maps-precategories
 open import category-theory.precategories
 
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equivalences
@@ -256,3 +259,118 @@ module _
       ( map-functor-Precategory C D H)
       ( map-functor-Precategory C D I)
 ```
+
+## Whiskering
+
+If `α : F ⇒ G` is a natural transformations between functors `F, G : C → D`, and
+`H : D → E` is another functor, we can form the natural transformation
+`H • α : H ∘ F ⇒ H ∘ G`. Its component at `x` is `(H • α)(x) = H(α(x))`.
+
+On the other hand, if we have a functor `K : B → C`, we can form a natural
+transformation `α • K : F ∘ K ⇒ G ∘ K`. Its component at `x` is
+`(α • K)(x) = α(K(x))`.
+
+Here, `•` denotes _whiskering_. Note that there are two kinds of whiskering,
+depending on whether the first or the second parameter expects a natural
+transformation.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {C : Precategory l1 l2}
+  {D : Precategory l3 l4}
+  {E : Precategory l5 l6}
+  where
+
+  whiskering-functor-natural-transformation-Precategory :
+    (F G : functor-Precategory C D)
+    (H : functor-Precategory D E)
+    (α : natural-transformation-Precategory C D F G) →
+    natural-transformation-Precategory
+      ( C)
+      ( 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 α =
+    ( λ x → (pr1 (pr2 H)) ((pr1 α) x)) ,
+    ( λ {x} {y} → λ f →
+      inv
+        ( preserves-comp-functor-Precategory
+          ( D)
+          ( E)
+          ( H)
+          ( (pr1 (pr2 G)) f)
+          ( (pr1 α) x)) ∙
+      ( ap (pr1 (pr2 H)) ((pr2 α) f)) ∙
+      ( preserves-comp-functor-Precategory
+        ( D)
+        ( E)
+        ( H)
+        ( (pr1 α) y)
+        ( (pr1 (pr2 F)) f)))
+
+  whiskering-natural-transformation-functor-Precategory :
+    (F G : functor-Precategory C D)
+    (α : natural-transformation-Precategory C D F G)
+    (K : functor-Precategory E C) →
+    natural-transformation-Precategory
+      ( E)
+      ( 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 =
+    (λ x → (pr1 α) ((pr1 K) x)) , (λ f → (pr2 α) ((pr1 (pr2 K)) f))
+```
+
+## Horizontal composition
+
+Horizontal composition (here denoted by `*`) is generalized
+[whiskering](category-theory.natural-transformations-functors-precategories.md#whiskering)
+(here denoted by `•`), and also defined by it. Given natural transformations
+`α : F ⇒ G`, `F, G : C → D`, and `β : H ⇒ I`, `H, I : D → E`, we can form a
+natural transformation `β * α : H ∘ F ⇒ I ∘ G`.
+
+More precisely, `β * α = (β • G) ∘ (H • α)`, that is, we compose two natural
+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}
+  where
+  horizontal-comp-natural-transformation-Precategory :
+    (F G : functor-Precategory C D)
+    (H I : functor-Precategory D E)
+    (β : natural-transformation-Precategory D E H I)
+    (α : natural-transformation-Precategory C D F G) →
+    natural-transformation-Precategory
+      ( C)
+      ( E)
+      ( 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-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)
+        ( α))
+```