Documentation Verification Report

PureCoherence

📁 Source: Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean

Statistics

Metric	Count
Definitions `instMkEqOfNaturalityBicategoryM`, `instMonadNormalizeNaturalityBicategoryM`, `normalizeIsoComp`, `pureCoherence`, `tacticBicategory_coherence`	5
Theorems `mk_eq_of_naturality`, `naturality_associator`, `naturality_comp`, `naturality_id`, `naturality_inv`, `naturality_leftUnitor`, `naturality_rightUnitor`, `naturality_whiskerLeft`, `naturality_whiskerRight`, `of_normalize_eq`	10
Total	15

Mathlib.Tactic.Bicategory

Definitions

Name	Category	Theorems
`instMkEqOfNaturalityBicategoryM` 📖	CompOp	—
`instMonadNormalizeNaturalityBicategoryM` 📖	CompOp	—
`normalizeIsoComp` 📖	CompOp	5 math math: `naturality_rightUnitor`, `naturality_whiskerRight`, `naturality_associator`, `naturality_whiskerLeft`, `naturality_leftUnitor`
`pureCoherence` 📖	CompOp	—
`tacticBicategory_coherence` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_eq_of_naturality` 📖	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Iso.trans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.whiskerLeftIso`	—	—	`Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Bicategory.id_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`
`naturality_associator` 📖	mathematical	—	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.whiskerLeftIso` `CategoryTheory.Bicategory.associator` `normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.whiskerRight_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv_assoc` `CategoryTheory.Bicategory.comp_whiskerRight`
`naturality_comp` 📖	—	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.whiskerLeftIso`	—	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.whiskerLeft_comp` `CategoryTheory.Category.assoc`
`naturality_id` 📖	mathematical	—	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.whiskerLeftIso` `CategoryTheory.Iso.refl`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.whiskerLeft_id` `CategoryTheory.Category.id_comp`
`naturality_inv` 📖	mathematical	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.whiskerLeftIso`	`CategoryTheory.Iso.symm`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.whiskerLeft_inv_hom_assoc`
`naturality_leftUnitor` 📖	mathematical	—	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.whiskerLeftIso` `CategoryTheory.Bicategory.leftUnitor` `normalizeIsoComp` `CategoryTheory.Bicategory.rightUnitor`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.triangle_assoc_comp_right_assoc`
`naturality_rightUnitor` 📖	mathematical	—	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.whiskerLeftIso` `CategoryTheory.Bicategory.rightUnitor` `normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.whiskerLeft_rightUnitor` `CategoryTheory.Category.assoc` `CategoryTheory.Bicategory.whiskerRight_id` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`naturality_whiskerLeft` 📖	mathematical	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.whiskerLeftIso`	`normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.comp_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc`
`naturality_whiskerRight` 📖	mathematical	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.whiskerLeftIso`	`CategoryTheory.Bicategory.whiskerRightIso` `normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.comp_whiskerRight` `CategoryTheory.Bicategory.whisker_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc`
`of_normalize_eq` 📖	—	`CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.whiskerLeftIso`	—	—	`CategoryTheory.Iso.ext` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Bicategory.id_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`

---

← Back to Index