InducedBicategory

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

Statistics

Metric	Count
Definitions InducedBicategory, category, hom, Hom₂, hom, bicategory, categoryStruct, forget, hasCoeToSort, isoMk, mkHom, mkHom₂	12
Theorems category_comp_hom, category_id_hom, ext, ext_iff, ext, ext_iff, bicategory_Hom, bicategory_associator_hom_hom, bicategory_associator_inv_hom, bicategory_comp_hom, bicategory_homCategory_comp_hom, bicategory_homCategory_id_hom, bicategory_id_hom, bicategory_leftUnitor_hom_hom, bicategory_leftUnitor_inv_hom, bicategory_rightUnitor_hom_hom, bicategory_rightUnitor_inv_hom, bicategory_whiskerLeft_hom, bicategory_whiskerRight_hom, categoryStruct_comp_hom, categoryStruct_id_hom, eqToHom_hom, forget_map, forget_mapComp_hom, forget_mapComp_inv, forget_mapId_hom, forget_mapId_inv, forget_map₂, forget_obj, hom_ext, hom_ext_iff, hom₂_ext, hom₂_ext_iff, instStrict, isoMk_hom_hom, isoMk_inv_hom, mkHom_eqToHom	37
Total	49

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
InducedBicategory 📖	CompOp	29 math math: InducedBicategory.bicategory_whiskerLeft_hom, InducedBicategory.bicategory_associator_inv_hom, InducedBicategory.Hom.category_id_hom, InducedBicategory.categoryStruct_comp_hom, InducedBicategory.bicategory_leftUnitor_inv_hom, InducedBicategory.eqToHom_hom, InducedBicategory.bicategory_whiskerRight_hom, InducedBicategory.forget_map, InducedBicategory.bicategory_comp_hom, InducedBicategory.bicategory_Hom, InducedBicategory.instStrict, InducedBicategory.bicategory_rightUnitor_hom_hom, InducedBicategory.bicategory_rightUnitor_inv_hom, InducedBicategory.forget_mapId_inv, InducedBicategory.forget_mapComp_inv, InducedBicategory.forget_mapComp_hom, InducedBicategory.bicategory_homCategory_comp_hom, InducedBicategory.forget_obj, InducedBicategory.Hom.category_comp_hom, InducedBicategory.isoMk_inv_hom, InducedBicategory.forget_map₂, InducedBicategory.bicategory_id_hom, InducedBicategory.bicategory_homCategory_id_hom, InducedBicategory.bicategory_associator_hom_hom, InducedBicategory.isoMk_hom_hom, InducedBicategory.mkHom_eqToHom, InducedBicategory.forget_mapId_hom, InducedBicategory.categoryStruct_id_hom, InducedBicategory.bicategory_leftUnitor_hom_hom

CategoryTheory.Bicategory.InducedBicategory

Definitions

Name	Category	Theorems
Hom₂ 📖	CompData	—
bicategory 📖	CompOp	21 math math: bicategory_whiskerLeft_hom, bicategory_associator_inv_hom, bicategory_leftUnitor_inv_hom, bicategory_whiskerRight_hom, forget_map, bicategory_comp_hom, bicategory_Hom, instStrict, bicategory_rightUnitor_hom_hom, bicategory_rightUnitor_inv_hom, forget_mapId_inv, forget_mapComp_inv, forget_mapComp_hom, bicategory_homCategory_comp_hom, forget_obj, forget_map₂, bicategory_id_hom, bicategory_homCategory_id_hom, bicategory_associator_hom_hom, forget_mapId_hom, bicategory_leftUnitor_hom_hom
categoryStruct 📖	CompOp	16 math math: bicategory_associator_inv_hom, Hom.category_id_hom, categoryStruct_comp_hom, bicategory_leftUnitor_inv_hom, eqToHom_hom, bicategory_rightUnitor_hom_hom, bicategory_rightUnitor_inv_hom, bicategory_homCategory_comp_hom, Hom.category_comp_hom, isoMk_inv_hom, bicategory_homCategory_id_hom, bicategory_associator_hom_hom, isoMk_hom_hom, mkHom_eqToHom, categoryStruct_id_hom, bicategory_leftUnitor_hom_hom
forget 📖	CompOp	7 math math: forget_map, forget_mapId_inv, forget_mapComp_inv, forget_mapComp_hom, forget_obj, forget_map₂, forget_mapId_hom
hasCoeToSort 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_inv_hom, isoMk_hom_hom
mkHom 📖	CompOp	3 math math: bicategory_whiskerLeft_hom, bicategory_whiskerRight_hom, mkHom_eqToHom
mkHom₂ 📖	CompOp	1 math math: mkHom_eqToHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bicategory_Hom 📖	mathematical	—	Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory Hom	—	—
bicategory_associator_hom_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct Hom.hom CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category CategoryTheory.Bicategory.associator bicategory CategoryTheory.Bicategory.homCategory	—	—
bicategory_associator_inv_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct Hom.hom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category CategoryTheory.Bicategory.associator bicategory CategoryTheory.Bicategory.homCategory	—	—
bicategory_comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.InducedBicategory CategoryTheory.Bicategory.toCategoryStruct bicategory	—	—
bicategory_homCategory_comp_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory bicategory CategoryTheory.Bicategory.toCategoryStruct Hom.hom	—	—
bicategory_homCategory_id_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory bicategory CategoryTheory.Bicategory.toCategoryStruct Hom.hom	—	—
bicategory_id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.InducedBicategory CategoryTheory.Bicategory.toCategoryStruct bicategory	—	—
bicategory_leftUnitor_hom_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id Hom.hom CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category CategoryTheory.Bicategory.leftUnitor bicategory CategoryTheory.Bicategory.homCategory	—	—
bicategory_leftUnitor_inv_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.CategoryStruct.id Hom.hom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category CategoryTheory.Bicategory.leftUnitor bicategory CategoryTheory.Bicategory.homCategory	—	—
bicategory_rightUnitor_hom_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category CategoryTheory.Bicategory.rightUnitor bicategory CategoryTheory.Bicategory.homCategory	—	—
bicategory_rightUnitor_inv_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category CategoryTheory.Bicategory.rightUnitor bicategory CategoryTheory.Bicategory.homCategory	—	—
bicategory_whiskerLeft_hom 📖	mathematical	—	Hom₂.hom mkHom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct Hom.hom CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Bicategory.InducedBicategory bicategory	—	—
bicategory_whiskerRight_hom 📖	mathematical	—	Hom₂.hom mkHom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct Hom.hom CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.InducedBicategory bicategory	—	—
categoryStruct_comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.InducedBicategory categoryStruct CategoryTheory.Bicategory.toCategoryStruct	—	—
categoryStruct_id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.InducedBicategory categoryStruct CategoryTheory.Bicategory.toCategoryStruct	—	—
eqToHom_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.eqToHom Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct CategoryTheory.Category.toCategoryStruct Hom.category CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Hom.hom	—	—
forget_map 📖	mathematical	—	Prefunctor.map CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget Hom.hom	—	—
forget_mapComp_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Prefunctor.obj CategoryTheory.Bicategory.InducedBicategory bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.StrictPseudofunctorPreCore.toPrelaxFunctor CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore Hom.hom Hom₂.hom Prefunctor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.mapComp CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget CategoryTheory.CategoryStruct.id	—	—
forget_mapComp_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Prefunctor.obj CategoryTheory.Bicategory.InducedBicategory bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.StrictPseudofunctorPreCore.toPrelaxFunctor CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore Hom.hom Hom₂.hom Prefunctor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.mapComp CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget CategoryTheory.CategoryStruct.id	—	—
forget_mapId_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Prefunctor.obj CategoryTheory.Bicategory.InducedBicategory bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.StrictPseudofunctorPreCore.toPrelaxFunctor CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore Hom.hom Hom₂.hom Prefunctor.map CategoryTheory.CategoryStruct.id CategoryTheory.Pseudofunctor.mapId CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget	—	—
forget_mapId_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct Prefunctor.obj CategoryTheory.Bicategory.InducedBicategory bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.StrictPseudofunctorPreCore.toPrelaxFunctor CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore Hom.hom Hom₂.hom Prefunctor.map CategoryTheory.CategoryStruct.id CategoryTheory.Pseudofunctor.mapId CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget	—	—
forget_map₂ 📖	mathematical	—	CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget Hom₂.hom	—	—
forget_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor forget	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom₂_ext 📖	—	Hom₂.hom	—	—	Hom₂.ext
hom₂_ext_iff 📖	mathematical	—	Hom₂.hom	—	hom₂_ext
instStrict 📖	mathematical	—	CategoryTheory.Bicategory.Strict CategoryTheory.Bicategory.InducedBicategory bicategory	—	hom_ext CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Iso.ext hom₂_ext CategoryTheory.Bicategory.Strict.id_comp CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso eqToHom_hom CategoryTheory.Bicategory.Strict.comp_id CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso CategoryTheory.Bicategory.Strict.assoc CategoryTheory.Bicategory.Strict.associator_eqToIso
isoMk_hom_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category isoMk CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Hom.hom	—	—
isoMk_inv_hom 📖	mathematical	—	Hom₂.hom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver categoryStruct Hom.category isoMk CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory Hom.hom	—	—
mkHom_eqToHom 📖	mathematical	—	mkHom₂ CategoryTheory.eqToHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.InducedBicategory categoryStruct Hom.category mkHom	—	hom₂_ext

CategoryTheory.Bicategory.InducedBicategory.Hom

Definitions

Name	Category	Theorems
category 📖	CompOp	12 math math: CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_inv_hom, category_id_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_inv_hom, CategoryTheory.Bicategory.InducedBicategory.eqToHom_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_hom_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_inv_hom, category_comp_hom, CategoryTheory.Bicategory.InducedBicategory.isoMk_inv_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_hom_hom, CategoryTheory.Bicategory.InducedBicategory.isoMk_hom_hom, CategoryTheory.Bicategory.InducedBicategory.mkHom_eqToHom, CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_hom_hom
hom 📖	CompOp	26 math math: CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerLeft_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_inv_hom, category_id_hom, CategoryTheory.Bicategory.InducedBicategory.categoryStruct_comp_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_inv_hom, CategoryTheory.Bicategory.InducedBicategory.eqToHom_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerRight_hom, CategoryTheory.Bicategory.InducedBicategory.forget_map, CategoryTheory.Bicategory.InducedBicategory.bicategory_comp_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_hom_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_inv_hom, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_inv, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_inv, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_hom, CategoryTheory.Bicategory.InducedBicategory.hom_ext_iff, CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_comp_hom, category_comp_hom, CategoryTheory.Bicategory.InducedBicategory.isoMk_inv_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_id_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_id_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_hom_hom, ext_iff, CategoryTheory.Bicategory.InducedBicategory.isoMk_hom_hom, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_hom, CategoryTheory.Bicategory.InducedBicategory.categoryStruct_id_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_hom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
category_comp_hom 📖	mathematical	—	CategoryTheory.Bicategory.InducedBicategory.Hom₂.hom CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.InducedBicategory.categoryStruct CategoryTheory.Category.toCategoryStruct category CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory hom	—	—
category_id_hom 📖	mathematical	—	CategoryTheory.Bicategory.InducedBicategory.Hom₂.hom CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.Bicategory.InducedBicategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.InducedBicategory.categoryStruct CategoryTheory.Category.toCategoryStruct category CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.homCategory hom	—	—
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext

CategoryTheory.Bicategory.InducedBicategory.Hom₂

Definitions

Name	Category	Theorems
hom 📖	CompOp	22 math math: CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerLeft_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_inv_hom, CategoryTheory.Bicategory.InducedBicategory.Hom.category_id_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_inv_hom, CategoryTheory.Bicategory.InducedBicategory.eqToHom_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerRight_hom, CategoryTheory.Bicategory.InducedBicategory.hom₂_ext_iff, CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_hom_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_inv_hom, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_inv, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_inv, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_comp_hom, CategoryTheory.Bicategory.InducedBicategory.Hom.category_comp_hom, CategoryTheory.Bicategory.InducedBicategory.isoMk_inv_hom, CategoryTheory.Bicategory.InducedBicategory.forget_map₂, CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_id_hom, CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_hom_hom, CategoryTheory.Bicategory.InducedBicategory.isoMk_hom_hom, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_hom, ext_iff, CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_hom_hom

Theorems

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

---

← Back to Index