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] :

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