LocallyGroupoid

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

Statistics

Metric	Count
Definitions IsLocallyGroupoid, Pith, as, categoryStruct, homGroupoid, inclusion, inst, instInhabited, pseudofunctorToPith, pseudofunctorToPithCompInclusionStrongIsoHom, pseudofunctorToPithCompInclusionStrongIsoInv, ofLaxFunctorToLocallyGroupoid, ofOplaxFunctorToLocallyGroupoid	13
Theorems associator_hom_iso, associator_inv_iso_hom, associator_inv_iso_inv, comp_of, comp₂_iso_hom, comp₂_iso_hom_assoc, comp₂_iso_inv, comp₂_iso_inv_assoc, hom₂_ext, hom₂_ext_iff, id_of, id₂_iso_hom, id₂_iso_inv, inclusion_mapComp, inclusion_mapId, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, leftUnitor_hom_iso, leftUnitor_inv_iso_hom, mk_as, pseudofunctorToPith_mapComp_hom_iso, pseudofunctorToPith_mapComp_inv_iso_hom, pseudofunctorToPith_mapComp_inv_iso_inv, pseudofunctorToPith_mapId_hom_iso, pseudofunctorToPith_mapId_inv_iso_hom, pseudofunctorToPith_mapId_inv_iso_inv, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, rightUnitor_hom_iso, rightUnitor_inv_iso_hom, rightUnitor_inv_iso_inv, whiskerLeft_iso_hom, whiskerLeft_iso_inv, whiskerRight_iso_hom, whiskerRight_iso_inv, ofLaxFunctorToLocallyGroupoid_mapCompIso_hom, ofLaxFunctorToLocallyGroupoid_mapCompIso_inv, ofLaxFunctorToLocallyGroupoid_mapIdIso_hom, ofLaxFunctorToLocallyGroupoid_mapIdIso_inv, ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom, ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv, ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom, ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv	46
Total	59

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
IsLocallyGroupoid 📖	MathDef	—
Pith 📖	CompData	35 math math: Pith.inclusion_mapComp, Pith.pseudofunctorToPith_mapId_hom_iso, Pith.comp_of, Pith.whiskerRight_iso_inv, Pith.leftUnitor_inv_iso_hom, Pith.comp₂_iso_hom_assoc, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, Pith.pseudofunctorToPith_mapId_inv_iso_inv, Pith.id₂_iso_inv, Pith.rightUnitor_hom_iso, Pith.pseudofunctorToPith_mapComp_inv_iso_inv, Pith.whiskerRight_iso_hom, Pith.rightUnitor_inv_iso_inv, Pith.associator_hom_iso, Pith.whiskerLeft_iso_hom, Pith.id₂_iso_hom, Pith.id_of, Pith.whiskerLeft_iso_inv, Pith.associator_inv_iso_inv, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, Pith.inclusion_mapId, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, Pith.comp₂_iso_hom, Pith.associator_inv_iso_hom, Pith.leftUnitor_hom_iso, Pith.rightUnitor_inv_iso_hom, Pith.comp₂_iso_inv_assoc, Pith.pseudofunctorToPith_mapId_inv_iso_hom, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, Pith.comp₂_iso_inv, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, Pith.pseudofunctorToPith_mapComp_inv_iso_hom, Pith.pseudofunctorToPith_mapComp_hom_iso

CategoryTheory.Bicategory.Pith

Definitions

Name	Category	Theorems
as 📖	CompOp	37 math math: inclusion_mapComp, pseudofunctorToPith_mapId_hom_iso, comp_of, whiskerRight_iso_inv, leftUnitor_inv_iso_hom, comp₂_iso_hom_assoc, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, pseudofunctorToPith_mapId_inv_iso_inv, id₂_iso_inv, rightUnitor_hom_iso, pseudofunctorToPith_mapComp_inv_iso_inv, whiskerRight_iso_hom, rightUnitor_inv_iso_inv, associator_hom_iso, whiskerLeft_iso_hom, id₂_iso_hom, id_of, hom₂_ext_iff, whiskerLeft_iso_inv, associator_inv_iso_inv, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, inclusion_mapId, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, comp₂_iso_hom, associator_inv_iso_hom, leftUnitor_hom_iso, rightUnitor_inv_iso_hom, comp₂_iso_inv_assoc, pseudofunctorToPith_mapId_inv_iso_hom, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, comp₂_iso_inv, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, mk_as, pseudofunctorToPith_mapComp_inv_iso_hom, pseudofunctorToPith_mapComp_hom_iso
categoryStruct 📖	CompOp	8 math math: comp_of, comp₂_iso_hom_assoc, id₂_iso_inv, id₂_iso_hom, id_of, comp₂_iso_hom, comp₂_iso_inv_assoc, comp₂_iso_inv
homGroupoid 📖	CompOp	6 math math: comp₂_iso_hom_assoc, id₂_iso_inv, id₂_iso_hom, comp₂_iso_hom, comp₂_iso_inv_assoc, comp₂_iso_inv
inclusion 📖	CompOp	5 math math: inclusion_mapComp, inclusion_mapId, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂
inst 📖	CompOp	27 math math: inclusion_mapComp, pseudofunctorToPith_mapId_hom_iso, whiskerRight_iso_inv, leftUnitor_inv_iso_hom, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, pseudofunctorToPith_mapId_inv_iso_inv, rightUnitor_hom_iso, pseudofunctorToPith_mapComp_inv_iso_inv, whiskerRight_iso_hom, rightUnitor_inv_iso_inv, associator_hom_iso, whiskerLeft_iso_hom, whiskerLeft_iso_inv, associator_inv_iso_inv, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, inclusion_mapId, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, associator_inv_iso_hom, leftUnitor_hom_iso, rightUnitor_inv_iso_hom, pseudofunctorToPith_mapId_inv_iso_hom, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, pseudofunctorToPith_mapComp_inv_iso_hom, pseudofunctorToPith_mapComp_hom_iso
instInhabited 📖	CompOp	—
pseudofunctorToPith 📖	CompOp	10 math math: pseudofunctorToPith_mapId_hom_iso, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, pseudofunctorToPith_mapId_inv_iso_inv, pseudofunctorToPith_mapComp_inv_iso_inv, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, pseudofunctorToPith_mapId_inv_iso_hom, pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, pseudofunctorToPith_mapComp_inv_iso_hom, pseudofunctorToPith_mapComp_hom_iso
pseudofunctorToPithCompInclusionStrongIsoHom 📖	CompOp	—
pseudofunctorToPithCompInclusionStrongIsoInv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_iso 📖	mathematical	—	CategoryTheory.CoreHom.iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Core.of CategoryTheory.Iso.hom CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.associator CategoryTheory.Bicategory.Pith inst	—	—
associator_inv_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.CoreHom.iso CategoryTheory.Iso.inv CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.associator CategoryTheory.Bicategory.Pith inst	—	—
associator_inv_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.associator CategoryTheory.Bicategory.Pith inst CategoryTheory.Iso.hom	—	—
comp_of 📖	mathematical	—	CategoryTheory.Core.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Pith categoryStruct	—	—
comp₂_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Pith categoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory homGroupoid	—	—
comp₂_iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.Iso.hom CategoryTheory.CoreHom.iso CategoryTheory.Bicategory.Pith categoryStruct CategoryTheory.Groupoid.toCategory homGroupoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp₂_iso_hom
comp₂_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Pith categoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory homGroupoid	—	—
comp₂_iso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.Iso.inv CategoryTheory.CoreHom.iso CategoryTheory.Bicategory.Pith categoryStruct CategoryTheory.Groupoid.toCategory homGroupoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp₂_iso_inv
hom₂_ext 📖	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CoreHom.iso	—	—	CategoryTheory.CoreHom.ext CategoryTheory.Iso.ext
hom₂_ext_iff 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CoreHom.iso	—	hom₂_ext
id_of 📖	mathematical	—	CategoryTheory.Core.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Pith categoryStruct	—	—
id₂_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Pith categoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory homGroupoid	—	—
id₂_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Pith categoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Groupoid.toCategory homGroupoid	—	—
inclusion_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.Bicategory.Pith inst inclusion CategoryTheory.Iso.refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp	—	—
inclusion_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.Bicategory.Pith inst inclusion CategoryTheory.Iso.refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.id	—	—
inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ 📖	mathematical	—	CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Bicategory.Pith CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct inst Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor inclusion CategoryTheory.Iso.hom as CategoryTheory.Core.of CategoryTheory.CoreHom.iso	—	—
inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.Bicategory.Pith CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor inclusion CategoryTheory.Core.of as	—	—
inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.Bicategory.Pith CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor inclusion as	—	—
leftUnitor_hom_iso 📖	mathematical	—	CategoryTheory.CoreHom.iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.Core.of CategoryTheory.Iso.hom CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.leftUnitor CategoryTheory.Bicategory.Pith inst	—	—
leftUnitor_inv_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.CoreHom.iso CategoryTheory.Iso.inv CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.leftUnitor CategoryTheory.Bicategory.Pith inst	—	—
mk_as 📖	mathematical	—	as	—	—
pseudofunctorToPith_mapComp_hom_iso 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.CoreHom.iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Prefunctor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Pith inst CategoryTheory.Iso.hom CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorToPith	—	—
pseudofunctorToPith_mapComp_inv_iso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Pith inst Prefunctor.map CategoryTheory.CoreHom.iso CategoryTheory.Iso.inv CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorToPith	—	—
pseudofunctorToPith_mapComp_inv_iso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Pith inst Prefunctor.map CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Pseudofunctor.mapComp pseudofunctorToPith CategoryTheory.Iso.hom	—	—
pseudofunctorToPith_mapId_hom_iso 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.CoreHom.iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Prefunctor.map CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Pith inst CategoryTheory.Iso.hom CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorToPith	—	—
pseudofunctorToPith_mapId_inv_iso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Core.of CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Pith inst Prefunctor.map CategoryTheory.CoreHom.iso CategoryTheory.Iso.inv CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorToPith	—	—
pseudofunctorToPith_mapId_inv_iso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Core.of CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.Pith inst Prefunctor.map CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Pseudofunctor.mapId pseudofunctorToPith CategoryTheory.Iso.hom	—	—
pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Core.of Prefunctor.map CategoryTheory.CoreHom.iso CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Bicategory.Pith inst pseudofunctorToPith	—	—
pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Core.of Prefunctor.map CategoryTheory.CoreHom.iso CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Bicategory.Pith inst pseudofunctorToPith CategoryTheory.inv	—	—
pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Core.of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as Prefunctor.obj CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Prefunctor.map CategoryTheory.Bicategory.Pith inst pseudofunctorToPith	—	—
pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	as Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Bicategory.Pith inst CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor pseudofunctorToPith	—	—
rightUnitor_hom_iso 📖	mathematical	—	CategoryTheory.CoreHom.iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Core.of CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.Bicategory.Pith inst	—	—
rightUnitor_inv_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.CoreHom.iso CategoryTheory.Iso.inv CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.Bicategory.Pith inst	—	—
rightUnitor_inv_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.Core.of CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.Bicategory.Pith inst CategoryTheory.Iso.hom	—	—
whiskerLeft_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Bicategory.Pith inst	—	—
whiskerLeft_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Bicategory.Pith inst	—	—
whiskerRight_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Pith inst	—	—
whiskerRight_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct as CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.Pith inst	—	—

CategoryTheory.Bicategory.Pseudofunctor

Definitions

Name	Category	Theorems
ofLaxFunctorToLocallyGroupoid 📖	CompOp	4 math math: ofLaxFunctorToLocallyGroupoid_mapCompIso_inv, ofLaxFunctorToLocallyGroupoid_mapIdIso_inv, ofLaxFunctorToLocallyGroupoid_mapIdIso_hom, ofLaxFunctorToLocallyGroupoid_mapCompIso_hom
ofOplaxFunctorToLocallyGroupoid 📖	CompOp	4 math math: ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom, ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv, ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv, ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofLaxFunctorToLocallyGroupoid_mapCompIso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom 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.CategoryStruct.comp CategoryTheory.LaxFunctor.PseudoCore.mapCompIso ofLaxFunctorToLocallyGroupoid CategoryTheory.inv CategoryTheory.LaxFunctor.mapComp	—	—
ofLaxFunctorToLocallyGroupoid_mapCompIso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv 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.CategoryStruct.comp CategoryTheory.LaxFunctor.PseudoCore.mapCompIso ofLaxFunctorToLocallyGroupoid CategoryTheory.LaxFunctor.mapComp	—	—
ofLaxFunctorToLocallyGroupoid_mapIdIso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom 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.CategoryStruct.id CategoryTheory.LaxFunctor.PseudoCore.mapIdIso ofLaxFunctorToLocallyGroupoid CategoryTheory.inv CategoryTheory.LaxFunctor.mapId	—	—
ofLaxFunctorToLocallyGroupoid_mapIdIso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv 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.CategoryStruct.id CategoryTheory.LaxFunctor.PseudoCore.mapIdIso ofLaxFunctorToLocallyGroupoid CategoryTheory.LaxFunctor.mapId	—	—
ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom 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.CategoryStruct.comp CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso ofOplaxFunctorToLocallyGroupoid CategoryTheory.OplaxFunctor.mapComp	—	—
ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv 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.CategoryStruct.comp CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso ofOplaxFunctorToLocallyGroupoid CategoryTheory.inv CategoryTheory.OplaxFunctor.mapComp	—	—
ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.hom 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.CategoryStruct.id CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso ofOplaxFunctorToLocallyGroupoid CategoryTheory.OplaxFunctor.mapId	—	—
ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv 📖	mathematical	CategoryTheory.Bicategory.IsLocallyGroupoid	CategoryTheory.Iso.inv 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.CategoryStruct.id CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso ofOplaxFunctorToLocallyGroupoid CategoryTheory.inv CategoryTheory.OplaxFunctor.mapId	—	—

---

← Back to Index