Commit 2023-04-02 16:48 c80a8514

View on Github →

feat: port CategoryTheory.Monad.Kleisli (#3209)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monad/Kleisli.lean

added def CategoryTheory.Cokleisli.Adjunction.adj

added def CategoryTheory.Cokleisli.Adjunction.fromCokleisli

added def CategoryTheory.Cokleisli.Adjunction.toCokleisli

added def CategoryTheory.Cokleisli.Adjunction.toCokleisliCompFromCokleisliIsoSelf

added def CategoryTheory.Cokleisli

added def CategoryTheory.Kleisli.Adjunction.adj

added def CategoryTheory.Kleisli.Adjunction.fromKleisli

added def CategoryTheory.Kleisli.Adjunction.toKleisli

added def CategoryTheory.Kleisli.Adjunction.toKleisliCompFromKleisliIsoSelf

added def CategoryTheory.Kleisli