Documentation Verification Report

Coherence

📁 Source: Mathlib/CategoryTheory/Bicategory/Coherence.lean

Statistics

Metric	Count
Definitions `homCategory'`, `inclusion`, `inclusionMapCompAux`, `inclusionPath`, `inclusionPathAux`, `normalize`, `normalizeAux`, `normalizeEquiv`, `normalizeIso`, `normalizeUnitIso`, `preinclusion`	11
Theorems `locally_thin`, `normalizeAux_congr`, `normalizeAux_nil_comp`, `normalize_naturality`, `preinclusion_map₂`, `preinclusion_obj`	6
Total	17

CategoryTheory.FreeBicategory

Definitions

Name	Category	Theorems
`homCategory'` 📖	CompOp	—
`inclusion` 📖	CompOp	—
`inclusionMapCompAux` 📖	CompOp	—
`inclusionPath` 📖	CompOp	—
`inclusionPathAux` 📖	CompOp	—
`normalize` 📖	CompOp	—
`normalizeAux` 📖	CompOp	3 math math: `normalizeAux_congr`, `normalize_naturality`, `normalizeAux_nil_comp`
`normalizeEquiv` 📖	CompOp	—
`normalizeIso` 📖	CompOp	1 math math: `normalize_naturality`
`normalizeUnitIso` 📖	CompOp	—
`preinclusion` 📖	CompOp	3 math math: `preinclusion_map₂`, `normalize_naturality`, `preinclusion_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locally_thin` 📖	mathematical	—	`Quiver.IsThin` `Quiver.Hom` `CategoryTheory.FreeBicategory` `quiver` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `homCategory`	—	`CategoryTheory.Functor.map_injective` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.Discrete.instSubsingletonDiscreteHom`
`normalizeAux_congr` 📖	mathematical	—	`normalizeAux`	—	—
`normalizeAux_nil_comp` 📖	mathematical	—	`normalizeAux` `Quiver.Path.nil` `Hom.comp` `Quiver.Path.comp`	—	`Quiver.Path.comp_assoc`
`normalize_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.FreeBicategory` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `bicategory` `Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `CategoryTheory.Paths` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `preinclusion` `homCategory` `Prefunctor.map` `CategoryTheory.LocallyDiscrete.as` `normalizeAux` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Iso.hom` `categoryStruct` `normalizeIso` `CategoryTheory.PrelaxFunctorStruct.map₂` `CategoryTheory.eqToHom` `CategoryTheory.Discrete.ext` `normalizeAux_congr`	—	`CategoryTheory.Discrete.ext` `normalizeAux_congr` `CategoryTheory.Bicategory.whiskerLeft_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Bicategory.whiskerLeft_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Discrete.eq_of_hom` `CategoryTheory.eqToHom_trans` `CategoryTheory.Bicategory.associator_inv_naturality_right_assoc` `CategoryTheory.Bicategory.whisker_exchange_assoc` `CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc` `CategoryTheory.Bicategory.comp_whiskerRight_assoc` `CategoryTheory.Bicategory.comp_whiskerRight` `CategoryTheory.dcongr_arg` `CategoryTheory.Bicategory.eqToHom_whiskerRight` `CategoryTheory.Bicategory.whiskerRight_comp` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv_assoc` `CategoryTheory.Bicategory.pentagon_inv_assoc` `CategoryTheory.Bicategory.whiskerLeft_rightUnitor` `CategoryTheory.Bicategory.whiskerRight_id` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Bicategory.triangle_assoc_comp_right_assoc` `CategoryTheory.Bicategory.whiskerLeft_inv_hom_assoc`
`preinclusion_map₂` 📖	mathematical	—	`CategoryTheory.PrelaxFunctorStruct.map₂` `CategoryTheory.LocallyDiscrete` `CategoryTheory.Paths` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Paths.categoryPaths` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.FreeBicategory` `bicategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `preinclusion` `CategoryTheory.eqToHom` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `homCategory` `Prefunctor.map` `CategoryTheory.Discrete` `Quiver.Path` `CategoryTheory.Discrete.ext` `CategoryTheory.Discrete.eq_of_hom`	—	—
`preinclusion_obj` 📖	mathematical	—	`Prefunctor.obj` `CategoryTheory.LocallyDiscrete` `CategoryTheory.Paths` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.FreeBicategory` `bicategory` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `Quiver.Hom` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `preinclusion`	—	—

---

← Back to Index