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]
Equations
- category_theory.Kleisli.category_struct = {to_has_hom := {hom := λ (α β : category_theory.Kleisli m), α → m β}, id := λ (α : category_theory.Kleisli m) (x : α), has_pure.pure x, comp := λ (X Y Z : category_theory.Kleisli m) (f : X ⟶ Y) (g : Y ⟶ Z), f >=> g}
@[instance]
Equations
- category_theory.Kleisli.category = {to_category_struct := {to_has_hom := {hom := λ (α β : category_theory.Kleisli m), α → m β}, id := λ (α : category_theory.Kleisli m) (x : α), has_pure.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) :
𝟙 α = has_pure.pure
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 : α) :