mathlib documentation

category_theory.category.Kleisli

def category_theory.Kleisli (m : Type u → Type v) [monad m] :

Type (u+1)

Equations

category_theory.Kleisli m = Type u

def category_theory.Kleisli.mk (m : Type u → Type v) [monad m] (α : Type u) :

category_theory.Kleisli m

Equations

category_theory.Kleisli.mk m α = α

@[instance]

def category_theory.Kleisli.category_struct {m : Type u_1 → Type u_2} [monad m] :

category_theory.category_struct (category_theory.Kleisli m)

Equations

category_theory.Kleisli.category_struct = {to_has_hom := {hom := λ (α β : category_theory.Kleisli m), α → m β}, id := λ (α : category_theory.Kleisli m) (x : α), pure x, comp := λ (X Y Z : category_theory.Kleisli m) (f : X ⟶ Y) (g : Y ⟶ Z), f >=> g}

@[instance]

def category_theory.Kleisli.category {m : Type u_1 → Type u_2} [monad m] [is_lawful_monad m] :

category_theory.category (category_theory.Kleisli m)

Equations

category_theory.Kleisli.category = {to_category_struct := {to_has_hom := {hom := λ (α β : category_theory.Kleisli m), α → m β}, id := λ (α : category_theory.Kleisli m) (x : α), pure x, comp := λ (X Y Z : category_theory.Kleisli m) (f : X ⟶ Y) (g : Y ⟶ Z), f >=> g}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.Kleisli.id_def {m : Type u_1 → Type u_2} [monad m] [is_lawful_monad m] (α : category_theory.Kleisli m) :

theorem category_theory.Kleisli.comp_def {m : Type u_1 → Type u_2} [monad m] [is_lawful_monad m] (α β γ : category_theory.Kleisli m) (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) :

(xs ≫ ys) a = xs a >>= ys