Documentation Verification Report

KleisliCat

📁 Source: Mathlib/CategoryTheory/Category/KleisliCat.lean

Statistics

Metric	Count
Definitions `KleisliCat`, `category`, `categoryStruct`, `mk`, `instInhabitedKleisliCatId`, `instInhabitedMkId`	6
Theorems `comp_def`, `ext`, `ext_iff`, `id_def`	4
Total	10

CategoryTheory

Definitions

Name	Category	Theorems
`KleisliCat` 📖	CompOp	12 math math: `eq_counitIso`, `Traversable.foldlm.ofFreeMonoid_comp_of`, `eq_functor_obj`, `eq_inverse_obj`, `Monoid.foldlM.ofFreeMonoid_apply`, `KleisliCat.id_def`, `eq_functor_map`, `Traversable.foldrm.ofFreeMonoid_comp_of`, `eq_unitIso`, `eq_inverse_map`, `Monoid.foldrM.ofFreeMonoid_apply`, `KleisliCat.comp_def`
`instInhabitedKleisliCatId` 📖	CompOp	—
`instInhabitedMkId` 📖	CompOp	—

CategoryTheory.KleisliCat

Definitions

Name	Category	Theorems
`category` 📖	CompOp	10 math math: `CategoryTheory.eq_counitIso`, `Traversable.foldlm.ofFreeMonoid_comp_of`, `CategoryTheory.eq_functor_obj`, `CategoryTheory.eq_inverse_obj`, `Monoid.foldlM.ofFreeMonoid_apply`, `CategoryTheory.eq_functor_map`, `Traversable.foldrm.ofFreeMonoid_comp_of`, `CategoryTheory.eq_unitIso`, `CategoryTheory.eq_inverse_map`, `Monoid.foldrM.ofFreeMonoid_apply`
`categoryStruct` 📖	CompOp	4 math math: `Traversable.foldlm.ofFreeMonoid_comp_of`, `Monoid.foldlM.ofFreeMonoid_apply`, `id_def`, `comp_def`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.KleisliCat` `categoryStruct`	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`id_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.KleisliCat` `categoryStruct`	—	—

---

← Back to Index