Documentation Verification Report

BicategoricalComp

📁 Source: Mathlib/Tactic/CategoryTheory/BicategoricalComp.lean

Statistics

Metric	Count
Definitions `BicategoricalCoherence`, `assoc`, `assoc'`, `iso`, `left`, `left'`, `refl`, `right`, `right'`, `tensorRight`, `tensorRight'`, `whiskerLeft`, `whiskerRight`, `«term_≪⊗≫_»`, `«term_⊗≫_»`, `«term⊗𝟙»`, `bicategoricalComp`, `bicategoricalIso`, `bicategoricalIsoComp`	19
Theorems `assoc'_iso`, `assoc_iso`, `left'_iso`, `left_iso`, `refl_iso`, `right'_iso`, `right_iso`, `tensorRight'_iso`, `tensorRight_iso`, `whiskerLeft_iso`, `whiskerRight_iso`, `bicategoricalComp_refl`	12
Total	31

CategoryTheory

Definitions

Name	Category	Theorems
`BicategoricalCoherence` 📖	CompData	—
`bicategoricalComp` 📖	CompOp	5 math math: `Mathlib.Tactic.Bicategory.StructuralOfExpr_bicategoricalComp`, `Bicategory.mateEquiv_symm_apply'`, `bicategoricalComp_refl`, `Bicategory.rightZigzag_idempotent_of_left_triangle`, `Bicategory.mateEquiv_apply'`
`bicategoricalIso` 📖	CompOp	—
`bicategoricalIsoComp` 📖	CompOp	1 math math: `Mathlib.Tactic.Bicategory.StructuralOfExpr_bicategoricalComp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bicategoricalComp_refl` 📖	mathematical	—	`bicategoricalComp` `BicategoricalCoherence.refl` `CategoryStruct.comp` `Quiver.Hom` `CategoryStruct.toQuiver` `Bicategory.toCategoryStruct` `Category.toCategoryStruct` `Bicategory.homCategory`	—	`Category.id_comp`

CategoryTheory.BicategoricalCoherence

Definitions

Name	Category	Theorems
`assoc` 📖	CompOp	3 math math: `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `assoc_iso`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`assoc'` 📖	CompOp	3 math math: `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `assoc'_iso`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`iso` 📖	CompOp	11 math math: `left'_iso`, `tensorRight_iso`, `left_iso`, `right'_iso`, `tensorRight'_iso`, `whiskerRight_iso`, `assoc_iso`, `assoc'_iso`, `right_iso`, `whiskerLeft_iso`, `refl_iso`
`left` 📖	CompOp	3 math math: `left_iso`, `CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`left'` 📖	CompOp	2 math math: `left'_iso`, `CategoryTheory.Bicategory.mateEquiv_symm_apply'`
`refl` 📖	CompOp	5 math math: `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `CategoryTheory.bicategoricalComp_refl`, `CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle`, `refl_iso`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`right` 📖	CompOp	2 math math: `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `right_iso`
`right'` 📖	CompOp	3 math math: `right'_iso`, `CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`tensorRight` 📖	CompOp	1 math math: `tensorRight_iso`
`tensorRight'` 📖	CompOp	1 math math: `tensorRight'_iso`
`whiskerLeft` 📖	CompOp	3 math math: `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `whiskerLeft_iso`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`whiskerRight` 📖	CompOp	3 math math: `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `whiskerRight_iso`, `CategoryTheory.Bicategory.mateEquiv_apply'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc'_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `assoc'` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Iso.symm` `CategoryTheory.Bicategory.associator`	—	—
`assoc_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `assoc` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.associator`	—	—
`left'_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.CategoryStruct.id` `left'` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Iso.symm` `CategoryTheory.Bicategory.leftUnitor`	—	—
`left_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.CategoryStruct.id` `left` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.leftUnitor`	—	—
`refl_iso` 📖	mathematical	—	`iso` `refl` `CategoryTheory.Iso.refl` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory`	—	—
`right'_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.CategoryStruct.id` `right'` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Iso.symm` `CategoryTheory.Bicategory.rightUnitor`	—	—
`right_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.CategoryStruct.id` `right` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.rightUnitor`	—	—
`tensorRight'_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `tensorRight'` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.whiskerLeftIso` `CategoryTheory.Bicategory.rightUnitor`	—	—
`tensorRight_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `tensorRight` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.symm` `CategoryTheory.Bicategory.rightUnitor` `CategoryTheory.Bicategory.whiskerLeftIso`	—	—
`whiskerLeft_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `whiskerLeft` `CategoryTheory.Bicategory.whiskerLeftIso`	—	—
`whiskerRight_iso` 📖	mathematical	—	`iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `whiskerRight` `CategoryTheory.Bicategory.whiskerRightIso`	—	—

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`«term_≪⊗≫_»` 📖	CompOp	—
`«term_⊗≫_»` 📖	CompOp	—
`«term⊗𝟙»` 📖	CompOp	—

---

← Back to Index