Def CategoryTheory.Kleisli.Adjunction.toKleisliCompFromKleisliIsoSelf

Modification history

2023-04-02 16:48
Mathlib/CategoryTheory/Monad/Kleisli.lean
feat: port CategoryTheory.Monad.Kleisli (#3209)
Added CategoryTheory.Kleisli.Adjunction.toKleisliCompFromKleisliIsoSelfView on Github →