Documentation Verification Report

Pseudo

📁 Source: Mathlib/CategoryTheory/Bicategory/Modification/Pseudo.lean

Statistics

Metric	Count
Definitions `as`, `Modification`, `app`, `equivOplax`, `hasCoeToOplax`, `id`, `instInhabited`, `mkOfOplax`, `toOplax`, `vcomp`, `homCategory`, `instInhabitedHom`, `isoMk`	13
Theorems `ext`, `ext_iff`, `equivOplax_apply`, `equivOplax_symm_apply`, `ext`, `ext_iff`, `id_app`, `mkOfOplax_app`, `naturality`, `naturality_assoc`, `toOplax_app`, `vcomp_app`, `whiskerLeft_naturality`, `whiskerLeft_naturality_assoc`, `whiskerRight_naturality`, `whiskerRight_naturality_assoc`, `ext`, `ext_iff`, `homCategory_comp_as_app`, `homCategory_id_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`	22
Total	35

CategoryTheory.Pseudofunctor.StrongTrans

Definitions

Name	Category	Theorems
`Modification` 📖	CompData	2 math math: `Modification.equivOplax_apply`, `Modification.equivOplax_symm_apply`
`homCategory` 📖	CompOp	10 math math: `homCategory_comp_as_app`, `leftUnitor_inv_as_app`, `homCategory_id_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`, `associator_inv_as_app`, `leftUnitor_hom_as_app`, `rightUnitor_inv_as_app`, `associator_hom_as_app`, `rightUnitor_hom_as_app`
`instInhabitedHom` 📖	CompOp	—
`isoMk` 📖	CompOp	2 math math: `isoMk_hom_as_app`, `isoMk_inv_as_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homCategory_comp_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.Pseudofunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `app`	—	—
`homCategory_id_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.Pseudofunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `app`	—	—
`isoMk_hom_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.Pseudofunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `app`	—	—
`isoMk_inv_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.Pseudofunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `app`	—	—

CategoryTheory.Pseudofunctor.StrongTrans.Hom

Definitions

Name	Category	Theorems
`as` 📖	CompOp	14 math math: `CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext_iff`, `ext_iff`, `CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`as`	—	—	—
`ext_iff` 📖	mathematical	—	`as`	—	`ext`

CategoryTheory.Pseudofunctor.StrongTrans.Modification

Definitions

Name	Category	Theorems
`app` 📖	CompOp	24 math math: `CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app`, `toOplax_app`, `CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app`, `whiskerLeft_naturality_assoc`, `CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext_iff`, `naturality`, `CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app`, `whiskerLeft_naturality`, `CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app`, `id_app`, `CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app`, `naturality_assoc`, `CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app`, `CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app`, `ext_iff`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app`, `mkOfOplax_app`, `vcomp_app`, `whiskerRight_naturality`, `whiskerRight_naturality_assoc`
`equivOplax` 📖	CompOp	2 math math: `equivOplax_apply`, `equivOplax_symm_apply`
`hasCoeToOplax` 📖	CompOp	—
`id` 📖	CompOp	1 math math: `id_app`
`instInhabited` 📖	CompOp	—
`mkOfOplax` 📖	CompOp	2 math math: `mkOfOplax_app`, `equivOplax_apply`
`toOplax` 📖	CompOp	2 math math: `toOplax_app`, `equivOplax_symm_apply`
`vcomp` 📖	CompOp	1 math math: `vcomp_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivOplax_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Oplax.StrongTrans.Modification` `CategoryTheory.Pseudofunctor.toOplax` `CategoryTheory.Pseudofunctor.StrongTrans.toOplax` `CategoryTheory.Pseudofunctor.StrongTrans.Modification` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOplax` `mkOfOplax`	—	—
`equivOplax_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Pseudofunctor.StrongTrans.Modification` `CategoryTheory.Oplax.StrongTrans.Modification` `CategoryTheory.Pseudofunctor.toOplax` `CategoryTheory.Pseudofunctor.StrongTrans.toOplax` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivOplax` `toOplax`	—	—
`ext` 📖	—	`app`	—	—	—
`ext_iff` 📖	mathematical	—	`app`	—	`ext`
`id_app` 📖	mathematical	—	`app` `id` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `CategoryTheory.Pseudofunctor.StrongTrans.app`	—	—
`mkOfOplax_app` 📖	mathematical	—	`app` `mkOfOplax` `CategoryTheory.Oplax.StrongTrans.Modification.app` `CategoryTheory.Pseudofunctor.toOplax` `CategoryTheory.Pseudofunctor.StrongTrans.toOplax`	—	—
`naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Pseudofunctor.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	—
`naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Pseudofunctor.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality`
`toOplax_app` 📖	mathematical	—	`CategoryTheory.Oplax.StrongTrans.Modification.app` `CategoryTheory.Pseudofunctor.toOplax` `CategoryTheory.Pseudofunctor.StrongTrans.toOplax` `toOplax` `app`	—	—
`vcomp_app` 📖	mathematical	—	`app` `vcomp` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `CategoryTheory.Pseudofunctor.StrongTrans.app`	—	—
`whiskerLeft_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Pseudofunctor.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality`
`whiskerLeft_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Pseudofunctor.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `whiskerLeft_naturality`
`whiskerRight_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Pseudofunctor.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality`	—	`CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality`
`whiskerRight_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.Pseudofunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Pseudofunctor.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator` `CategoryTheory.Iso.hom` `CategoryTheory.Pseudofunctor.StrongTrans.naturality`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `whiskerRight_naturality`

CategoryTheory.Pseudofunctor.StrongTrans.homCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.Pseudofunctor.StrongTrans.Modification.app` `CategoryTheory.Pseudofunctor.StrongTrans.Hom.as`	—	—	`CategoryTheory.Pseudofunctor.StrongTrans.Hom.ext` `CategoryTheory.Pseudofunctor.StrongTrans.Modification.ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.Pseudofunctor.StrongTrans.Modification.app` `CategoryTheory.Pseudofunctor.StrongTrans.Hom.as`	—	`ext`

---

← Back to Index