mathlib documentation

category_theory.monad.types

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.

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

@[simp]
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) :