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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          X ⨿ - has a monad structure. This is sometimes called the either monad.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For