Documentation Verification Report

Oplax

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

Statistics

Metric	Count
Definitions `as`, `Modification`, `app`, `id`, `instInhabited`, `vcomp`, `ofComponents`, `homCategory`, `instInhabitedHomOplaxFunctor`, `isoMk`, `as`, `Modification`, `app`, `equivOplax`, `hasCoeToOplax`, `id`, `instInhabited`, `mkOfOplax`, `toOplax`, `vcomp`, `homCategory`, `instInhabitedHomOplaxFunctor`, `isoMk`	23
Theorems `ext`, `ext_iff`, `ext`, `ext_iff`, `id_app`, `naturality`, `naturality_assoc`, `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`, `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`	40
Total	63

CategoryTheory.Oplax.OplaxTrans

Definitions

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

CategoryTheory.Oplax.OplaxTrans.Hom

Definitions

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

Theorems

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

CategoryTheory.Oplax.OplaxTrans.Modification

Definitions

Name	Category	Theorems
`app` 📖	CompOp	32 math math: `whiskerRight_naturality`, `CategoryTheory.Oplax.OplaxTrans.homCategory.ext_iff`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app`, `vcomp_app`, `CategoryTheory.Oplax.OplaxTrans.homCategory_id_as_app`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app`, `CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app`, `CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app`, `CategoryTheory.Oplax.StrongTrans.Modification.toOplax_app`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app`, `whiskerLeft_naturality_assoc`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app`, `CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app`, `CategoryTheory.Oplax.OplaxTrans.homCategory_comp_as_app`, `naturality_assoc`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app`, `CategoryTheory.Oplax.OplaxTrans.isoMk_hom_as_app`, `CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app`, `whiskerRight_naturality_assoc`, `CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app`, `CategoryTheory.Oplax.OplaxTrans.isoMk_inv_as_app`, `CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app`, `whiskerLeft_naturality`, `ext_iff`, `naturality`, `CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplax_app`, `CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app`, `CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app`, `CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app`, `id_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.OplaxFunctor.toPrelaxFunctor` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `CategoryTheory.Oplax.OplaxTrans.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Oplax.OplaxTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Oplax.OplaxTrans.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator` `CategoryTheory.Oplax.OplaxTrans.naturality`	—	`CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc` `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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.OplaxTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator` `CategoryTheory.Oplax.OplaxTrans.naturality`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `whiskerRight_naturality`

CategoryTheory.Oplax.OplaxTrans.ModificationIso

Definitions

Name	Category	Theorems
`ofComponents` 📖	CompOp	—

CategoryTheory.Oplax.OplaxTrans.homCategory

Theorems

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

CategoryTheory.Oplax.StrongTrans

Definitions

Name	Category	Theorems
`Modification` 📖	CompData	4 math math: `Modification.equivOplax_symm_apply`, `Modification.equivOplax_apply`, `CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_apply`, `CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_symm_apply`
`homCategory` 📖	CompOp	4 math math: `homCategory_id_as_app`, `isoMk_hom_as_app`, `isoMk_inv_as_app`, `homCategory_comp_as_app`
`instInhabitedHomOplaxFunctor` 📖	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.OplaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.OplaxFunctor.toPrelaxFunctor` `app`	—	—
`homCategory_id_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.OplaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.OplaxFunctor.toPrelaxFunctor` `app`	—	—
`isoMk_hom_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.OplaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.OplaxFunctor.toPrelaxFunctor` `app`	—	—
`isoMk_inv_as_app` 📖	mathematical	—	`Modification.app` `Hom.as` `CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.OplaxFunctor` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `homCategory` `isoMk` `CategoryTheory.Bicategory.toCategoryStruct` `Prefunctor.obj` `CategoryTheory.PrelaxFunctorStruct.toPrefunctor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct` `CategoryTheory.OplaxFunctor.toPrelaxFunctor` `app`	—	—

CategoryTheory.Oplax.StrongTrans.Hom

Definitions

Name	Category	Theorems
`as` 📖	CompOp	6 math math: `CategoryTheory.Oplax.StrongTrans.homCategory_id_as_app`, `CategoryTheory.Oplax.StrongTrans.isoMk_hom_as_app`, `CategoryTheory.Oplax.StrongTrans.homCategory.ext_iff`, `ext_iff`, `CategoryTheory.Oplax.StrongTrans.isoMk_inv_as_app`, `CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app`

Theorems

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

CategoryTheory.Oplax.StrongTrans.Modification

Definitions

Name	Category	Theorems
`app` 📖	CompOp	18 math math: `vcomp_app`, `CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax_app`, `whiskerLeft_naturality`, `CategoryTheory.Oplax.StrongTrans.homCategory_id_as_app`, `whiskerRight_naturality`, `toOplax_app`, `naturality_assoc`, `id_app`, `CategoryTheory.Oplax.StrongTrans.isoMk_hom_as_app`, `CategoryTheory.Oplax.StrongTrans.homCategory.ext_iff`, `CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax_app`, `CategoryTheory.Oplax.StrongTrans.isoMk_inv_as_app`, `naturality`, `whiskerLeft_naturality_assoc`, `whiskerRight_naturality_assoc`, `ext_iff`, `CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app`, `mkOfOplax_app`
`equivOplax` 📖	CompOp	2 math math: `equivOplax_symm_apply`, `equivOplax_apply`
`hasCoeToOplax` 📖	CompOp	—
`id` 📖	CompOp	1 math math: `id_app`
`instInhabited` 📖	CompOp	—
`mkOfOplax` 📖	CompOp	2 math math: `equivOplax_apply`, `mkOfOplax_app`
`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.OplaxTrans.Modification` `CategoryTheory.Oplax.StrongTrans.toOplax` `CategoryTheory.Oplax.StrongTrans.Modification` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOplax` `mkOfOplax`	—	—
`equivOplax_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Oplax.StrongTrans.Modification` `CategoryTheory.Oplax.OplaxTrans.Modification` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `CategoryTheory.Oplax.StrongTrans.app`	—	—
`mkOfOplax_app` 📖	mathematical	—	`app` `mkOfOplax` `CategoryTheory.Oplax.OplaxTrans.Modification.app` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Oplax.StrongTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality`
`toOplax_app` 📖	mathematical	—	`CategoryTheory.Oplax.OplaxTrans.Modification.app` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Oplax.StrongTrans.naturality` `CategoryTheory.Bicategory.whiskerRight`	—	`CategoryTheory.Oplax.OplaxTrans.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Oplax.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator` `CategoryTheory.Iso.hom` `CategoryTheory.Oplax.StrongTrans.naturality`	—	`CategoryTheory.Oplax.OplaxTrans.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.OplaxFunctor.toPrelaxFunctor` `Prefunctor.map` `CategoryTheory.Oplax.StrongTrans.app` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.whiskerRight` `app` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator` `CategoryTheory.Iso.hom` `CategoryTheory.Oplax.StrongTrans.naturality`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `whiskerRight_naturality`

CategoryTheory.Oplax.StrongTrans.homCategory

Theorems

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

---

← Back to Index