Documentation

Mathlib.CategoryTheory.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.

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.

                Instances For