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.

@[simp]
theorem category_theory.of_type_monad_μ_app (m : Type uType u) [monad m] [is_lawful_monad m] {α : Type u} (a : m (m α)) :
def category_theory.of_type_monad (m : Type uType u) [monad m] [is_lawful_monad m] :

A lawful control.monad gives a category theory monad on the category of types.

Equations
@[simp]
theorem category_theory.of_type_monad_η_app (m : Type uType u) [monad m] [is_lawful_monad m] {α : Type u} (ᾰ : α) :

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_inverse_map (m : Type uType u) [monad m] [is_lawful_monad m] (X Y : category_theory.kleisli (category_theory.of_type_monad m)) (f : X Y) (ᾰ : X) :
@[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) (ᾰ : X) :