# Monads on precategories

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2024-02-06.

module category-theory.monads-on-precategories where

Imports
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
open import foundation.identity-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types


## Idea

A monad on a precategory C consists of an endofunctor T : C → C together with two natural transformations: η : 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 monad laws:

• Associativity: μ ∘ (T • μ) = μ ∘ (μ • T)
• The left unit law: μ ∘ (T • η) = 1_T
• The right unit law: μ ∘ (η • T) = 1_T.

Here, • denotes whiskering, and 1_T : T ⇒ T denotes the identity natural transformation for T.

## Definitions

### Multiplication structure on a pointed endofunctor on a precategory

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

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

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

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

module _
{l1 l2 : Level} (C : Precategory l1 l2)
(T : pointed-endofunctor-Precategory C)
where

structure-monad-pointed-endofunctor-Precategory : UU (l1 ⊔ l2)
Σ ( 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

module _
{l1 l2 : Level} (C : Precategory l1 l2)
where

monad-Precategory : UU (l1 ⊔ l2)
Σ ( pointed-endofunctor-Precategory C)

module _
where

pointed-endofunctor-Precategory C
pointed-endofunctor-monad-Precategory = pr1 T

functor-Precategory C C
functor-pointed-endofunctor-Precategory C

obj-Precategory C → obj-Precategory C
obj-functor-Precategory C C endofunctor-monad-Precategory

{X Y : obj-Precategory C} →
hom-Precategory C X Y →
hom-Precategory C
hom-functor-Precategory C C endofunctor-monad-Precategory

(X : obj-Precategory C) →
hom-endofunctor-monad-Precategory (id-hom-Precategory C {X}) ＝
id-hom-Precategory C
preserves-id-functor-Precategory C C 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
preserves-comp-functor-Precategory C C

pointing-pointed-endofunctor-Precategory C

hom-family-functor-Precategory C C
( id-functor-Precategory C)
hom-family-pointing-pointed-endofunctor-Precategory C

is-natural-transformation-Precategory C C
( id-functor-Precategory C)
naturality-pointing-pointed-endofunctor-Precategory C

structure-multiplication-pointed-endofunctor-Precategory C
mul-monad-Precategory = pr1 (pr2 T)

hom-family-functor-Precategory C C
( comp-functor-Precategory C C C
hom-family-natural-transformation-Precategory C C
( comp-functor-Precategory C C C

is-natural-transformation-Precategory C C
( comp-functor-Precategory C C C
naturality-natural-transformation-Precategory C C
( comp-functor-Precategory C C C

associative-mul-pointed-endofunctor-Precategory C
pr1 (pr2 (pr2 T))

left-unit-law-mul-pointed-endofunctor-Precategory C