mathlib documentation


The Kleisli construction on the Type category #

Define the Kleisli category for (control) monads. category_theory/monad/kleisli defines the general version for a monad on C, and demonstrates the equivalence between the two.


Generalise this to work with category_theory.monad

def category_theory.Kleisli (m : Type uType v) :
Type (u+1)

The Kleisli category on the (type-)monad m. Note that the monad is not assumed to be lawful yet.

def (m : Type uType u_1) (α : Type u) :

Construct an object of the Kleisli category from a type.

theorem category_theory.Kleisli.id_def {m : Type u_1Type u_2} [monad m] (α : category_theory.Kleisli m) :
theorem category_theory.Kleisli.comp_def {m : Type u_1Type u_2} [monad m] (α β γ : category_theory.Kleisli m) (xs : α β) (ys : β γ) (a : α) :
(xs ys) a = xs a >>= ys