Documentation Verification Report

EqToHom

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

Statistics

Metric	Count
Definitions `eqToHomTransIso`	1
Theorems `associator_eqToHom_hom`, `associator_eqToHom_hom_assoc`, `associator_eqToHom_inv`, `associator_eqToHom_inv_assoc`, `associator_hom_congr`, `associator_inv_congr`, `congr_whiskerLeft`, `eqToHomTransIso_refl_left`, `eqToHomTransIso_refl_refl`, `eqToHomTransIso_refl_right`, `leftUnitor_hom_congr`, `leftUnitor_inv_congr`, `rightUnitor_hom_congr`, `rightUnitor_inv_congr`, `whiskerRight_congr`	15
Total	16

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`eqToHomTransIso` 📖	CompOp	7 math math: `eqToHomTransIso_refl_left`, `eqToHomTransIso_refl_refl`, `associator_eqToHom_hom_assoc`, `associator_eqToHom_inv`, `eqToHomTransIso_refl_right`, `associator_eqToHom_inv_assoc`, `associator_eqToHom_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_eqToHom_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.eqToHom` `associator` `CategoryTheory.Category.toCategoryStruct` `whiskerRight` `CategoryTheory.Iso.inv` `eqToHomTransIso` `whiskerLeft`	—	`unitors_equal` `whiskerRight_id` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id` `unitors_inv_equal` `whiskerLeft_rightUnitor_inv` `CategoryTheory.Iso.hom_inv_id_assoc`
`associator_eqToHom_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.eqToHom` `CategoryTheory.Iso.hom` `associator` `whiskerRight` `CategoryTheory.Iso.inv` `eqToHomTransIso` `whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `associator_eqToHom_hom`
`associator_eqToHom_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.eqToHom` `associator` `CategoryTheory.Category.toCategoryStruct` `whiskerLeft` `eqToHomTransIso` `CategoryTheory.Iso.hom` `whiskerRight`	—	`unitors_equal` `whiskerLeft_rightUnitor` `unitors_inv_equal` `whiskerRight_id` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`associator_eqToHom_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.eqToHom` `CategoryTheory.Iso.inv` `associator` `whiskerLeft` `eqToHomTransIso` `CategoryTheory.Iso.hom` `whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `associator_eqToHom_inv`
`associator_hom_congr` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `associator` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`associator_inv_congr` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `associator` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`congr_whiskerLeft` 📖	mathematical	—	`whiskerLeft` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.eqToHom`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`eqToHomTransIso_refl_left` 📖	mathematical	—	`eqToHomTransIso` `CategoryTheory.Iso.symm` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.eqToHom` `leftUnitor`	—	`CategoryTheory.Iso.ext` `unitors_inv_equal`
`eqToHomTransIso_refl_refl` 📖	mathematical	—	`eqToHomTransIso` `CategoryTheory.Iso.symm` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftUnitor`	—	—
`eqToHomTransIso_refl_right` 📖	mathematical	—	`eqToHomTransIso` `CategoryTheory.Iso.symm` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.eqToHom` `CategoryTheory.CategoryStruct.id` `rightUnitor`	—	`CategoryTheory.Iso.ext` `unitors_inv_equal`
`leftUnitor_hom_congr` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftUnitor` `CategoryTheory.Category.toCategoryStruct` `whiskerLeft` `CategoryTheory.eqToHom`	—	`whiskerLeft_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`leftUnitor_inv_congr` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftUnitor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom` `whiskerLeft`	—	`whiskerLeft_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`rightUnitor_hom_congr` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `rightUnitor` `CategoryTheory.Category.toCategoryStruct` `whiskerRight` `CategoryTheory.eqToHom`	—	`whiskerRight_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`rightUnitor_inv_congr` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `rightUnitor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom` `whiskerRight`	—	`whiskerRight_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`whiskerRight_congr` 📖	mathematical	—	`whiskerRight` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.eqToHom`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`

---

← Back to Index