Documentation

Mathlib.CategoryTheory.Monad.Kleisli

Kleisli category on a (co)monad #

This file defines the Kleisli category on a monad (T, η_ T, μ_ T) as well as the co-Kleisli category on a comonad (U, ε_ U, δ_ U). It also defines the Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T) as well as the co-Kleisli adjunction which gives rise to the comonad (U, ε_ U, δ_ U).

References #

The objects for the Kleisli category of the monad T : Monad C, which are the same thing as objects of the base category C.

Instances For

    The Kleisli category on a monad T. cf Definition 5.2.9 in [Riehl][riehl2017].

    The left adjoint of the adjunction which induces the monad (T, η_ T, μ_ T).

    Instances For

      The right adjoint of the adjunction which induces the monad (T, η_ T, μ_ T).

      Instances For

        The Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T). cf Lemma 5.2.11 of [Riehl][riehl2017].

        Instances For

          The objects for the co-Kleisli category of the comonad U : Comonad C, which are the same thing as objects of the base category C.

          Instances For

            The right adjoint of the adjunction which induces the comonad (U, ε_ U, δ_ U).

            Instances For

              The left adjoint of the adjunction which induces the comonad (U, ε_ U, δ_ U).

              Instances For