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.


Generalise this to work with CategoryTheory.Monad

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.

Instances For

    Construct an object of the Kleisli category from a type.

    Instances For
      theorem CategoryTheory.KleisliCat.comp_def {m : Type u_1 → Type u_2} [Monad m] (α : CategoryTheory.KleisliCat m) (β : CategoryTheory.KleisliCat m) (γ : CategoryTheory.KleisliCat m) (xs : α β) (ys : β γ) (a : α) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.KleisliCat m) CategoryTheory.KleisliCat.categoryStruct α β γ xs ys a = xs a >>= ys