mathlib

545f0fb9 - feat(category_theory/monad/kleisli): dualise kleisli of monad to cokleisli of comonad (#14799)

feat(category_theory/monad/kleisli): dualise kleisli of monad to cokleisli of comonad (#14799) This PR defines the (co)Kleisli category of a comonad, defines the corresponding adjunction, and proves that it gives rise to the original comonad.