mathlib documentation

category_theory.monad.kleisli

Kleisli category on a monad #

This file defines the Kleisli category on a monad (T, η_ T, μ_ T). It also defines the Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T).

References #

@[nolint]

The objects for the Kleisli category of the functor (usually monad) T : C ⥤ C, which are the same thing as objects of the base category C.

Equations
@[instance]

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

Equations

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

Equations

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

Equations