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
The Kleisli category on the (type-)monad m
. Note that the monad is not assumed to be lawful
yet.
Equations
Construct an object of the Kleisli category from a type.
Equations
Equations
- CategoryTheory.KleisliCat.categoryStruct = CategoryTheory.CategoryStruct.mk (fun x x_1 => pure x_1) fun {X Y Z} f g => f >=> g
instance
CategoryTheory.KleisliCat.category
{m : Type u → Type v}
[inst : Monad m]
[inst : LawfulMonad m]
:
Equations
- CategoryTheory.KleisliCat.category = CategoryTheory.Category.mk
@[simp]
theorem
CategoryTheory.KleisliCat.id_def
{m : Type u_1 → Type u_2}
[inst : Monad m]
(α : CategoryTheory.KleisliCat m)
:
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
Equations
- CategoryTheory.instInhabitedKleisliCatIdType = { default := PUnit }
Equations
- CategoryTheory.instInhabitedMkIdType = { default := let_fun this := default; this }