Documentation Verification Report

Lax

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

Statistics

Metric	Count
Definitions `as`, `Modification`, `app`, `id`, `instInhabited`, `vcomp`, `homCategory`, `instInhabitedHomLaxFunctor`, `isoMk`, `as`, `Modification`, `app`, `id`, `instInhabited`, `vcomp`, `homCategory`, `instInhabitedHomLaxFunctor`, `isoMk`	18
Theorems `ext`, `ext_iff`, `ext`, `ext_iff`, `id_app`, `naturality`, `naturality_assoc`, `vcomp_app`, `ext`, `ext_iff`, `homCategory_comp_as_app`, `homCategory_id_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`, `ext`, `ext_iff`, `ext`, `ext_iff`, `id_app`, `naturality`, `naturality_assoc`, `vcomp_app`, `ext`, `ext_iff`, `homCategory_comp_as_app`, `homCategory_id_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`	28
Total	46

CategoryTheory.Lax.LaxTrans

Definitions

Name	Category	Theorems
`Modification` 📖	CompData	—
`homCategory` 📖	CompOp	16 math math: `LaxFunctor.bicategory_rightUnitor_inv_as_app`, `associator_inv_as_app`, `leftUnitor_hom_as_app`, `rightUnitor_hom_as_app`, `LaxFunctor.bicategory_rightUnitor_hom_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`, `homCategory_comp_as_app`, `LaxFunctor.bicategory_leftUnitor_hom_as_app`, `homCategory_id_as_app`, `LaxFunctor.bicategory_leftUnitor_inv_as_app`, `leftUnitor_inv_as_app`, `LaxFunctor.bicategory_associator_hom_as_app`, `LaxFunctor.bicategory_associator_inv_as_app`, `associator_hom_as_app`, `rightUnitor_inv_as_app`
`instInhabitedHomLaxFunctor` 📖	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.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—
`homCategory_id_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—
`isoMk_hom_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—
`isoMk_inv_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—

CategoryTheory.Lax.LaxTrans.Hom

Definitions

Name	Category	Theorems
`as` 📖	CompOp	22 math math: `CategoryTheory.Lax.LaxTrans.whiskerLeft_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app`, `CategoryTheory.Lax.LaxTrans.associator_inv_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerRight_as_app`, `CategoryTheory.Lax.LaxTrans.homCategory.ext_iff`, `CategoryTheory.Lax.LaxTrans.leftUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.rightUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app`, `ext_iff`, `CategoryTheory.Lax.LaxTrans.whiskerRight_as_app`, `CategoryTheory.Lax.LaxTrans.isoMk_hom_as_app`, `CategoryTheory.Lax.LaxTrans.isoMk_inv_as_app`, `CategoryTheory.Lax.LaxTrans.homCategory_comp_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.homCategory_id_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app`, `CategoryTheory.Lax.LaxTrans.leftUnitor_inv_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_hom_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_inv_as_app`, `CategoryTheory.Lax.LaxTrans.associator_hom_as_app`, `CategoryTheory.Lax.LaxTrans.rightUnitor_inv_as_app`

Theorems

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

CategoryTheory.Lax.LaxTrans.Modification

Definitions

Name	Category	Theorems
`app` 📖	CompOp	26 math math: `CategoryTheory.Lax.LaxTrans.whiskerLeft_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app`, `CategoryTheory.Lax.LaxTrans.associator_inv_as_app`, `id_app`, `vcomp_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerRight_as_app`, `CategoryTheory.Lax.LaxTrans.homCategory.ext_iff`, `CategoryTheory.Lax.LaxTrans.leftUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.rightUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.whiskerRight_as_app`, `CategoryTheory.Lax.LaxTrans.isoMk_hom_as_app`, `CategoryTheory.Lax.LaxTrans.isoMk_inv_as_app`, `CategoryTheory.Lax.LaxTrans.homCategory_comp_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app`, `CategoryTheory.Lax.LaxTrans.homCategory_id_as_app`, `naturality_assoc`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app`, `CategoryTheory.Lax.LaxTrans.leftUnitor_inv_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_hom_as_app`, `CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_inv_as_app`, `CategoryTheory.Lax.LaxTrans.associator_hom_as_app`, `CategoryTheory.Lax.LaxTrans.rightUnitor_inv_as_app`, `naturality`, `ext_iff`
`id` 📖	CompOp	1 math math: `id_app`
`instInhabited` 📖	CompOp	—
`vcomp` 📖	CompOp	1 math math: `vcomp_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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.LaxFunctor.toPrelaxFunctor` `CategoryTheory.Lax.LaxTrans.app`	—	—
`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.LaxFunctor.toPrelaxFunctor` `CategoryTheory.Lax.LaxTrans.app` `Prefunctor.map` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Lax.LaxTrans.naturality` `CategoryTheory.Bicategory.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.LaxFunctor.toPrelaxFunctor` `CategoryTheory.Lax.LaxTrans.app` `Prefunctor.map` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Lax.LaxTrans.naturality` `CategoryTheory.Bicategory.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality`
`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.LaxFunctor.toPrelaxFunctor` `CategoryTheory.Lax.LaxTrans.app`	—	—

CategoryTheory.Lax.LaxTrans.homCategory

Theorems

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

CategoryTheory.Lax.OplaxTrans

Definitions

Name	Category	Theorems
`Modification` 📖	CompData	—
`homCategory` 📖	CompOp	16 math math: `rightUnitor_inv_as_app`, `rightUnitor_hom_as_app`, `LaxFunctor.bicategory_rightUnitor_hom_as_app`, `homCategory_id_as_app`, `associator_hom_as_app`, `homCategory_comp_as_app`, `associator_inv_as_app`, `LaxFunctor.bicategory_leftUnitor_hom_as_app`, `LaxFunctor.bicategory_associator_hom_as_app`, `LaxFunctor.bicategory_associator_inv_as_app`, `leftUnitor_hom_as_app`, `leftUnitor_inv_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`, `LaxFunctor.bicategory_leftUnitor_inv_as_app`, `LaxFunctor.bicategory_rightUnitor_inv_as_app`
`instInhabitedHomLaxFunctor` 📖	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.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—
`homCategory_id_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—
`isoMk_hom_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—
`isoMk_inv_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.LaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructLaxFunctor` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.LaxFunctor.toPrelaxFunctor` `app`	—	—

CategoryTheory.Lax.OplaxTrans.Hom

Definitions

Name	Category	Theorems
`as` 📖	CompOp	22 math math: `CategoryTheory.Lax.OplaxTrans.rightUnitor_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.rightUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.homCategory.ext_iff`, `CategoryTheory.Lax.OplaxTrans.whiskerRight_as_app`, `CategoryTheory.Lax.OplaxTrans.homCategory_id_as_app`, `CategoryTheory.Lax.OplaxTrans.associator_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.homCategory_comp_as_app`, `CategoryTheory.Lax.OplaxTrans.associator_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerRight_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_inv_as_app`, `ext_iff`, `CategoryTheory.Lax.OplaxTrans.leftUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.whiskerLeft_as_app`, `CategoryTheory.Lax.OplaxTrans.leftUnitor_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.isoMk_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.isoMk_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app`

Theorems

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

CategoryTheory.Lax.OplaxTrans.Modification

Definitions

Name	Category	Theorems
`app` 📖	CompOp	26 math math: `id_app`, `CategoryTheory.Lax.OplaxTrans.rightUnitor_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.rightUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.homCategory.ext_iff`, `CategoryTheory.Lax.OplaxTrans.whiskerRight_as_app`, `CategoryTheory.Lax.OplaxTrans.homCategory_id_as_app`, `naturality`, `vcomp_app`, `CategoryTheory.Lax.OplaxTrans.associator_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.homCategory_comp_as_app`, `CategoryTheory.Lax.OplaxTrans.associator_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerRight_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.leftUnitor_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.whiskerLeft_as_app`, `CategoryTheory.Lax.OplaxTrans.leftUnitor_inv_as_app`, `naturality_assoc`, `CategoryTheory.Lax.OplaxTrans.isoMk_hom_as_app`, `CategoryTheory.Lax.OplaxTrans.isoMk_inv_as_app`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app`, `ext_iff`, `CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app`
`id` 📖	CompOp	1 math math: `id_app`
`instInhabited` 📖	CompOp	—
`vcomp` 📖	CompOp	1 math math: `vcomp_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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.LaxFunctor.toPrelaxFunctor` `CategoryTheory.Lax.OplaxTrans.app`	—	—
`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.LaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Lax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Lax.OplaxTrans.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.LaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Lax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Lax.OplaxTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality`
`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.LaxFunctor.toPrelaxFunctor` `CategoryTheory.Lax.OplaxTrans.app`	—	—

CategoryTheory.Lax.OplaxTrans.homCategory

Theorems

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

---

← Back to Index