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

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.9

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

Construct an object of the Kleisli category from a type.

Equations

• CategoryTheory.KleisliCat.mk m α = α

instance CategoryTheory.KleisliCat.categoryStruct {m : Type u → Type v} [Monad m] : CategoryStruct.{max u v, u + 1} (KleisliCat m)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.KleisliCat.ext {m : Type u → Type v} [Monad m] (α β : KleisliCat m) (f g : α ⟶ β) (h : ∀ (x : α), f x = g x) : f = g

theorem CategoryTheory.KleisliCat.ext_iff {m : Type u → Type v} [Monad m] {α β : KleisliCat m} {f g : α ⟶ β} : f = g ↔ ∀ (x : α), f x = g x

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

Equations

• CategoryTheory.KleisliCat.category = { toCategoryStruct := CategoryTheory.KleisliCat.categoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[simp]

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

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

instance CategoryTheory.instInhabitedKleisliCatId : Inhabited (KleisliCat id)

Equations

• CategoryTheory.instInhabitedKleisliCatId = { default := PUnit.{?u.4 + 1} }

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

Equations

• CategoryTheory.instInhabitedMkId = { default := have this := default; this }