mathlib documentation

category_theory.category.Kleisli

def category_theory.Kleisli (m : Type uType v) [monad m] :
Type (u+1)
Equations
def category_theory.Kleisli.mk (m : Type uType v) [monad m] (α : Type u) :
Equations
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem category_theory.Kleisli.id_def {m : Type u_1Type u_2} [monad m] [is_lawful_monad m] (α : category_theory.Kleisli m) :
theorem category_theory.Kleisli.comp_def {m : Type u_1Type u_2} [monad m] [is_lawful_monad m] (α β γ : category_theory.Kleisli m) (xs : α β) (ys : β γ) (a : α) :
(xs ys) a = xs a >>= ys