The Kleisli construction on the Type category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

TODO #

Generalise this to work with category_theory.monad

source

@[nolint]

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

Type (u+1)

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

Equations

category_theory.Kleisli m = Type u

Instances for category_theory.Kleisli

source

def category_theory.Kleisli.mk (m : Type u → Type u_1) (α : Type u) :

category_theory.Kleisli m

Construct an object of the Kleisli category from a type.

Equations

category_theory.Kleisli.mk m α = α

Instances for category_theory.Kleisli.mk

category_theory.Kleisli.mk.inhabited

source

@[protected, instance]

def category_theory.Kleisli.category_struct {m : Type u → Type v} [monad m] :

category_theory.category_struct (category_theory.Kleisli m)

Equations

category_theory.Kleisli.category_struct = {to_quiver := {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}

source

@[protected, instance]

def category_theory.Kleisli.category {m : Type u → Type v} [monad m] [is_lawful_monad m] :

category_theory.category (category_theory.Kleisli m)

Equations

category_theory.Kleisli.category = {to_category_struct := category_theory.Kleisli.category_struct _inst_1, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

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

𝟙 α = has_pure.pure

source

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

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

source

@[protected, instance]

def category_theory.Kleisli.inhabited :

inhabited (category_theory.Kleisli id)

Equations

category_theory.Kleisli.inhabited = {default := punit}

source

@[protected, instance]

def category_theory.Kleisli.mk.inhabited {α : Type u} [inhabited α] :

inhabited (category_theory.Kleisli.mk id α)

Equations

category_theory.Kleisli.mk.inhabited = {default := show α, from inhabited.default}