Content created by Egbert Rijke and Gregor Perčič.

Created on 2024-02-06.

module category-theory.monads-on-categories where

Imports
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-categories

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 category 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 category

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

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

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

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

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

structure-monad-pointed-endofunctor-Category : UU (l1 ⊔ l2)
( precategory-Category C)
( T)


### The type of monads on categories

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

monad-Category : UU (l1 ⊔ l2)

module _
where

pointed-endofunctor-Category C

functor-Category C C

obj-Category C → obj-Category C

{X Y : obj-Category C} →
hom-Category C X Y →
hom-Category C

(X : obj-Category C) →
id-hom-Category C

{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-family-functor-Category C C
( id-functor-Category C)

is-natural-transformation-Category C C
( id-functor-Category C)

structure-multiplication-pointed-endofunctor-Category C

hom-family-functor-Category C C
( comp-functor-Category C C C

is-natural-transformation-Category C C
( comp-functor-Category C C C

associative-mul-pointed-endofunctor-Category C

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