Mathlib v3 is deprecated. Go to Mathlib v4

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