Monads #
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 CategoryTheory.Monad.Types
.)
For the fact that monads are "just" monoids in the category of endofunctors, see the file
CategoryTheory.Monad.EquivMon
.
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
- map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
The unit for the monad.
The multiplication for the monad.
- left_unit (X : C) : CategoryStruct.comp (self.η.app (self.obj X)) (self.μ.app X) = CategoryStruct.id ((Functor.id C).obj (self.obj X))
- right_unit (X : C) : CategoryStruct.comp (self.map (self.η.app X)) (self.μ.app X) = CategoryStruct.id (self.obj ((Functor.id C).obj X))
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)
- obj : C → C
- map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
The counit for the comonad.
The comultiplication for the comonad.
- left_counit (X : C) : CategoryStruct.comp (self.δ.app X) (self.ε.app (self.obj X)) = CategoryStruct.id (self.obj X)
- right_counit (X : C) : CategoryStruct.comp (self.δ.app X) (self.map (self.ε.app X)) = CategoryStruct.id (self.obj X)
Equations
- CategoryTheory.coeMonad = { coe := fun (T : CategoryTheory.Monad C) => T.toFunctor }
Equations
- CategoryTheory.coeComonad = { coe := fun (G : CategoryTheory.Comonad C) => G.toFunctor }
A morphism of monads is a natural transformation compatible with η and μ.
- naturality ⦃X Y : C⦄ (f : X ⟶ Y) : CategoryStruct.comp (T₁.map f) (self.app Y) = CategoryStruct.comp (self.app X) (T₂.map f)
- app_μ (X : C) : CategoryStruct.comp (T₁.μ.app X) (self.app X) = CategoryStruct.comp (CategoryStruct.comp (T₁.map (self.app X)) (self.app (T₂.obj X))) (T₂.μ.app X)
A morphism of comonads is a natural transformation compatible with ε and δ.
- naturality ⦃X Y : C⦄ (f : X ⟶ Y) : CategoryStruct.comp (M.map f) (self.app Y) = CategoryStruct.comp (self.app X) (N.map f)
- app_δ (X : C) : CategoryStruct.comp (self.app X) (N.δ.app X) = CategoryStruct.comp (M.δ.app X) (CategoryStruct.comp (self.app (M.obj X)) (N.map (self.app X)))
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
Construct a monad isomorphism from a natural isomorphism of functors where the forward direction is a monad morphism.
Equations
- One or more equations did not get rendered due to their size.
Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism.
Equations
- One or more equations did not get rendered due to their size.
The forgetful functor from the category of monads to the category of endofunctors.
Equations
- CategoryTheory.monadToFunctor C = { obj := fun (T : CategoryTheory.Monad C) => T.toFunctor, map := fun {X Y : CategoryTheory.Monad C} (f : X ⟶ Y) => f.toNatTrans, map_id := ⋯, map_comp := ⋯ }
The forgetful functor from the category of comonads to the category of endofunctors.
Equations
- One or more equations did not get rendered due to their size.
An isomorphism of monads gives a natural isomorphism of the underlying functors.
Equations
An isomorphism of comonads gives a natural isomorphism of the underlying functors.
Equations
The identity monad.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Monad.instInhabited C = { default := CategoryTheory.Monad.id C }
The identity comonad.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Comonad.instInhabited C = { default := CategoryTheory.Comonad.id C }
Transport a monad structure on a functor along an isomorphism of functors.
Equations
- One or more equations did not get rendered due to their size.
Transport a comonad structure on a functor along an isomorphism of functors.
Equations
- One or more equations did not get rendered due to their size.