Mathlib Map

Theorems · Definition · category theory

CategoryTheory.KleisliCat.mk

(m : Type u → Type u_1) → Type u → CategoryTheory.KleisliCat m

Construct an object of the Kleisli category from a type.

Defined in
Mathlib.CategoryTheory.Category.KleisliCat
Cited by
4 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Monoid.foldlM.ofFreeMonoid · cited by 3foldlM.ofFreeMonoidMonoid.foldrM.ofFreeMonoid · cited by 3foldrM.ofFreeMonoidMonoid.foldlM · cited by 2Monoid.foldlMMonoid.foldrM · cited by 2Monoid.foldrMTraversable.foldlm.ofFreeMonoid_comp_of · cited by 1foldlm.ofFreeMonoid_comp_…Traversable.foldrm.ofFreeMonoid_comp_of · cited by 1foldrm.ofFreeMonoid_comp_…Monoid.foldlM.ofFreeMonoid_apply · cited by 0foldlM.ofFreeMonoid_applyMonoid.foldrM.ofFreeMonoid_apply · cited by 0foldrM.ofFreeMonoid_applyCategoryTheory.KleisliCat · cited by 14CategoryTheory.KleisliCatKleisliCat.mkCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by8

Results whose statement or proof uses this declaration.