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
.
- obj : C → C
- map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
- map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
- η' : CategoryTheory.Functor.id C ⟶ s.toFunctor
- μ' : CategoryTheory.Functor.comp s.toFunctor s.toFunctor ⟶ s.toFunctor
- assoc' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.map (s.μ'.app X)) (s.μ'.app X) = CategoryTheory.CategoryStruct.comp (s.μ'.app (s.obj X)) (s.μ'.app X)
- left_unit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.η'.app (s.obj X)) (s.μ'.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (s.obj X))
- right_unit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.map (s.η'.app X)) (s.μ'.app X) = CategoryTheory.CategoryStruct.id (s.obj ((CategoryTheory.Functor.id C).obj X))
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)
Instances For
- obj : C → C
- map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
- map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
- ε' : s.toFunctor ⟶ CategoryTheory.Functor.id C
- δ' : s.toFunctor ⟶ CategoryTheory.Functor.comp s.toFunctor s.toFunctor
- coassoc' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.map (s.δ'.app X)) = CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.δ'.app (s.obj X))
- left_counit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.ε'.app (s.obj X)) = CategoryTheory.CategoryStruct.id (s.obj X)
- right_counit' : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.δ'.app X) (s.map (s.ε'.app X)) = CategoryTheory.CategoryStruct.id (s.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)
Instances For
The unit for the monad T
.
Instances For
The multiplication for the monad T
.
Instances For
The counit for the comonad G
.
Instances For
The comultiplication for the comonad G
.
Instances For
A custom simps projection for the functor part of a monad, as a coercion.
Instances For
A custom simps projection for the unit of a monad, in simp normal form.
Instances For
A custom simps projection for the multiplication of a monad, in simp normal form.
Instances For
A custom simps projection for the functor part of a comonad, as a coercion.
Instances For
A custom simps projection for the counit of a comonad, in simp normal form.
Instances For
A custom simps projection for the comultiplication of a comonad, in simp normal form.
Instances For
- app : (X : C) → T₁.obj X ⟶ T₂.obj X
- naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (T₁.map f) (s.app Y) = CategoryTheory.CategoryStruct.comp (s.app X) (T₂.map f)
- app_η : ∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T₁).app X) (s.app X) = (CategoryTheory.Monad.η T₂).app X
- app_μ : ∀ (X : C), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T₁).app X) (s.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T₁.map (s.app X)) (s.app (T₂.obj X))) ((CategoryTheory.Monad.μ T₂).app X)
A morphism of monads is a natural transformation compatible with η and μ.
Instances For
- app : (X : C) → M.obj X ⟶ N.obj X
- naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M.map f) (s.app Y) = CategoryTheory.CategoryStruct.comp (s.app X) (N.map f)
- app_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.app X) ((CategoryTheory.Comonad.ε N).app X) = (CategoryTheory.Comonad.ε M).app X
- app_δ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (s.app X) ((CategoryTheory.Comonad.δ N).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ M).app X) (CategoryTheory.CategoryStruct.comp (s.app (M.obj X)) (N.map (s.app X)))
A morphism of comonads is a natural transformation compatible with ε and δ.
Instances For
Construct a monad isomorphism from a natural isomorphism of functors where the forward direction is a monad morphism.
Instances For
Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism.
Instances For
The forgetful functor from the category of monads to the category of endofunctors.
Instances For
The forgetful functor from the category of comonads to the category of endofunctors.
Instances For
An isomorphism of monads gives a natural isomorphism of the underlying functors.
Instances For
An isomorphism of comonads gives a natural isomorphism of the underlying functors.
Instances For
The identity monad.
Instances For
The identity comonad.