Commit 2020-10-16 16:28 0d9227f8

feat(category_theory/monad/kleisli): add Kleisli category of a monad (#4542) Adds the Kleisli category of a monad, and shows the Kleisli category for a lawful control monad is equivalent to the Kleisli category of its category-theoretic version. Following discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/kleisli.20vs.20kleisli. I'd appreciate suggestions for names more sensible than the ones already there.