We construct the categories of monads and comonads, and their forgetful functors to endofunctors.
(Note that these are the category theorist's monads, not the programmers monads.
For the translation, see the file
For the fact that monads are "just" monoids in the category of endofunctors, see the file
- obj : C → C
The data of a monad on C consists of an endofunctor T together with natural transformations η : 𝟭 C ⟶ T and μ : T ⋙ T ⟶ T satisfying three equations:
- T μ_X ≫ μ_X = μ_(TX) ≫ μ_X (associativity)
- η_(TX) ≫ μ_X = 1_X (left unit)
- Tη_X ≫ μ_X = 1_X (right unit)
- obj : C → C
The data of a comonad on C consists of an endofunctor G together with natural transformations ε : G ⟶ 𝟭 C and δ : G ⟶ G ⋙ G satisfying three equations:
- δ_X ≫ G δ_X = δ_X ≫ δ_(GX) (coassociativity)
- δ_X ≫ ε_(GX) = 1_X (left counit)
- δ_X ≫ G ε_X = 1_X (right counit)
- app : (X : C) → T₁.obj X ⟶ T₂.obj X
A morphism of monads is a natural transformation compatible with η and μ.
- app : (X : C) → M.obj X ⟶ N.obj X
A morphism of comonads is a natural transformation compatible with ε and δ.
Construct a monad isomorphism from a natural isomorphism of functors where the forward direction is a monad morphism.
Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism.