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 #
- [Riehl, Category theory in context, Definition 5.2.9][riehl2017]
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 composition of the adjunction gives the original functor.
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 co-Kleisli category on a comonad U
.
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
The co-Kleisli adjunction which gives rise to the monad (U, ε_ U, δ_ U)
.
Instances For
The composition of the adjunction gives the original functor.