Kleisli categories #32
Description
This is a roadmap for facts about Kleisli categories, which we should promptly send off to mathlib after proving.
- Kleisli category
- Kleisli adjunction
- Category Adj(T) of adjunctions inducing the monad T
- That the Kleisli adjunction and the Eilenberg-Moore adjunction (already in mathlib) are respectively initial and terminal in Adj(T) (5.2.12 here)