Commit 2022-06-17 16:27 545f0fb9

View on Github →

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.

Estimated changes

Modified src/category_theory/monad/kleisli.lean

added def category_theory.cokleisli.adjunction.adj

added def category_theory.cokleisli.adjunction.from_cokleisli

added def category_theory.cokleisli.adjunction.to_cokleisli

added def category_theory.cokleisli.adjunction.to_cokleisli_comp_from_cokleisli_iso_self

added def category_theory.cokleisli