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.
X ⨯ -
has a comonad structure. This is sometimes called the writer comonad.
Instances For
The forward direction of the equivalence from coalgebras for the product comonad to the over category.
Instances For
The backward direction of the equivalence from coalgebras for the product comonad to the over category.
Instances For
The equivalence from coalgebras for the product comonad to the over category.
Instances For
X ⨿ -
has a monad structure. This is sometimes called the either monad.
Instances For
The forward direction of the equivalence from algebras for the coproduct monad to the under category.
Instances For
The backward direction of the equivalence from algebras for the coproduct monad to the under category.
Instances For
The equivalence from algebras for the coproduct monad to the under category.