mathlib documentation


Convert from monad (i.e. Lean's Type-based monads) to category_theory.monad

This allows us to use these monads in category theory.

The Kleisli category of a control.monad is equivalent to the kleisli category of its category-theoretic version, provided the monad is lawful.

theorem category_theory.eq_functor_obj (m : Type uType u) [monad m] [is_lawful_monad m] (X : category_theory.Kleisli m) :

theorem category_theory.eq_inverse_map (m : Type uType u) [monad m] [is_lawful_monad m] (X Y : category_theory.kleisli (category_theory.of_type_functor m)) (f : X Y) (ᾰ : X) :

theorem category_theory.eq_functor_map (m : Type uType u) [monad m] [is_lawful_monad m] (X Y : category_theory.Kleisli m) (f : X Y) (ᾰ : X) :