The Kleisli construction on the Type category

Define the Kleisli category for (control) monads. CategoryTheory/Monad/Kleisli defines the general version for a monad on C, and demonstrates the equivalence between the two.

TODO

Generalise this to work with CategoryTheory.Monad

ink

def CategoryTheory.KleisliCat : (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

• CategoryTheory.KleisliCat x = Type u

ink

def CategoryTheory.KleisliCat.mk (m : Type u → Type u_1) (α : Type u) : CategoryTheory.KleisliCat m

Construct an object of the Kleisli category from a type.

Equations

• CategoryTheory.KleisliCat.mk m α = α

ink

instance CategoryTheory.KleisliCat.categoryStruct {m : Type u → Type v} [inst : Monad m] : CategoryTheory.CategoryStruct (CategoryTheory.KleisliCat m)

Equations

• CategoryTheory.KleisliCat.categoryStruct = CategoryTheory.CategoryStruct.mk (fun x x_1 => pure x_1) fun {X Y Z} f g => f >=> g

ink

instance CategoryTheory.KleisliCat.category {m : Type u → Type v} [inst : Monad m] [inst : LawfulMonad m] : CategoryTheory.Category (CategoryTheory.KleisliCat m)

Equations

• CategoryTheory.KleisliCat.category = CategoryTheory.Category.mk

ink

@[simp]

theorem CategoryTheory.KleisliCat.id_def {m : Type u_1 → Type u_2} [inst : Monad m] (α : CategoryTheory.KleisliCat m) : 𝟙 α = pure

ink

theorem CategoryTheory.KleisliCat.comp_def {m : Type u_1 → Type u_2} [inst : Monad m] (α : CategoryTheory.KleisliCat m) (β : CategoryTheory.KleisliCat m) (γ : CategoryTheory.KleisliCat m) (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) : (CategoryTheory.KleisliCat m ≫ CategoryTheory.KleisliCat.categoryStruct) α β γ xs ys a = xs a >>= ys

ink

instance CategoryTheory.instInhabitedKleisliCatIdType : Inhabited (CategoryTheory.KleisliCat id)

Equations

• CategoryTheory.instInhabitedKleisliCatIdType = { default := PUnit }

ink

instance CategoryTheory.instInhabitedMkIdType {α : Type u} [inst : Inhabited α] : Inhabited (CategoryTheory.KleisliCat.mk id α)

Equations

• CategoryTheory.instInhabitedMkIdType = { default := let_fun this := default; this }