Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Bicategory/Strict/Basic.lean

Statistics

Metric	Count
Definitions `category`	1
Theorems `assoc`, `associator_eqToIso`, `comp_id`, `id_comp`, `leftUnitor_eqToIso`, `rightUnitor_eqToIso`, `eqToHom_whiskerRight`, `whiskerLeft_eqToHom`	8
Total	9

CategoryTheory.Bicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqToHom_whiskerRight` 📖	mathematical	—	`whiskerRight` `CategoryTheory.eqToHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp`	—	`id_whiskerRight`
`whiskerLeft_eqToHom` 📖	mathematical	—	`whiskerLeft` `CategoryTheory.eqToHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp`	—	`whiskerLeft_id`

CategoryTheory.Bicategory.Strict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct`	—	—
`associator_eqToIso` 📖	mathematical	—	`CategoryTheory.Bicategory.associator` `CategoryTheory.eqToIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `assoc`	—	—
`comp_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.CategoryStruct.id`	—	—
`id_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.CategoryStruct.id`	—	—
`leftUnitor_eqToIso` 📖	mathematical	—	`CategoryTheory.Bicategory.leftUnitor` `CategoryTheory.eqToIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `id_comp`	—	—
`rightUnitor_eqToIso` 📖	mathematical	—	`CategoryTheory.Bicategory.rightUnitor` `CategoryTheory.eqToIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `comp_id`	—	—

CategoryTheory.StrictBicategory

Definitions

Name	Category	Theorems
`category` 📖	CompOp	13 math math: `CategoryTheory.Functor.toPseudoFunctor'_obj`, `CategoryTheory.Functor.toOplaxFunctor'_obj`, `CategoryTheory.Functor.toPseudoFunctor'_map`, `CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id`, `CategoryTheory.CommSq.toLoc`, `CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id`, `CategoryTheory.StrictPseudofunctor.toFunctor_obj`, `CategoryTheory.Functor.toOplaxFunctor'_map`, `CategoryTheory.StrictPseudofunctor.toFunctor_map`, `CategoryTheory.Functor.toPseudoFunctor'_mapId`, `CategoryTheory.Functor.toPseudoFunctor'_mapComp`, `CategoryTheory.Functor.toOplaxFunctor'_mapComp`, `CategoryTheory.Functor.toOplaxFunctor'_mapId`

---

← Back to Index