mathlib documentation

category_theory.monad.products

Algebras for the coproduct monad #

The functor Y ↦ X ⨿ Y forms a monad, whose category of monads is equivalent to the under category of X. Similarly, Y ↦ X ⨯ Y forms a comonad, whose category of comonads is equivalent to the over category of X.

TODO #

Show that over.forget X : over X ⥤ C is a comonadic left adjoint and under.forget : under X ⥤ C is a monadic right adjoint.

The forward direction of the equivalence from coalgebras for the product comonad to the over category.

Equations

The backward direction of the equivalence from coalgebras for the product comonad to the over category.

Equations

The forward direction of the equivalence from algebras for the coproduct monad to the under category.

Equations

The backward direction of the equivalence from algebras for the coproduct monad to the under category.

Equations