DescentDataPrime

📁 Source: Mathlib/CategoryTheory/Sites/Descent/DescentDataPrime.lean

Statistics

Metric	Count
Definitions DescentData', hom, descentData, descentDataEquivalence, fromDescentDataFunctor, hom, instCategory, instQuiver, isoMk, obj, ofDescentData, pullHom', toDescentDataFunctor	13
Theorems comm, comm_assoc, ext, ext_iff, comm, comm_assoc, comp_hom, comp_hom_assoc, comp_pullHom', comp_pullHom'', comp_pullHom''_assoc, comp_pullHom'_assoc, descentDataEquivalence_counitIso, descentDataEquivalence_functor, descentDataEquivalence_inverse, descentDataEquivalence_unitIso, descentData_hom, descentData_obj, fromDescentDataFunctor_map_hom, fromDescentDataFunctor_obj, hom_ext, hom_ext_iff, id_hom, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, isoMk_hom_hom, isoMk_inv_hom, ofDescentData_hom, ofDescentData_obj, pullHom'_eq_hom, pullHom'_eq_pullHom, pullHom'_eq_pullHom_assoc, pullHom'_hom_comp, pullHom'_hom_comp_assoc, pullHom'_hom_self, pullHom'_ofDescentData_hom, pullHom'_p₁_p₂, pullHom'_self, pullHom'_self', pullHom'₁₂_eq_pullHom_of_chosenPullback₃, pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, pullHom'₁₃_eq_pullHom_of_chosenPullback₃, pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, pullHom'₂₃_eq_pullHom_of_chosenPullback₃, pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, pullHom_pullHom', pullHom_pullHom'_assoc, toDescentDataFunctor_map_hom, toDescentDataFunctor_obj	49
Total	62

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
DescentData' 📖	CompData	13 math math: DescentData'.toDescentDataFunctor_obj, DescentData'.descentDataEquivalence_inverse, DescentData'.comp_hom, DescentData'.isoMk_inv_hom, DescentData'.comp_hom_assoc, DescentData'.isoMk_hom_hom, DescentData'.toDescentDataFunctor_map_hom, DescentData'.descentDataEquivalence_unitIso, DescentData'.descentDataEquivalence_functor, DescentData'.fromDescentDataFunctor_map_hom, DescentData'.descentDataEquivalence_counitIso, DescentData'.fromDescentDataFunctor_obj, DescentData'.id_hom

CategoryTheory.Pseudofunctor.DescentData'

Definitions

Name	Category	Theorems
descentData 📖	CompOp	4 math math: toDescentDataFunctor_obj, toDescentDataFunctor_map_hom, descentData_hom, descentData_obj
descentDataEquivalence 📖	CompOp	4 math math: descentDataEquivalence_inverse, descentDataEquivalence_unitIso, descentDataEquivalence_functor, descentDataEquivalence_counitIso
fromDescentDataFunctor 📖	CompOp	5 math math: descentDataEquivalence_inverse, descentDataEquivalence_unitIso, fromDescentDataFunctor_map_hom, descentDataEquivalence_counitIso, fromDescentDataFunctor_obj
hom 📖	CompOp	16 math math: comm, comp_pullHom', instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, ofDescentData_hom, Hom.comm, pullHom'_hom_self, Hom.comm_assoc, pullHom'_eq_hom, pullHom'_hom_comp, comm_assoc, pullHom'_self, descentData_hom, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom, comp_pullHom'_assoc, pullHom'_hom_comp_assoc, pullHom'_ofDescentData_hom
instCategory 📖	CompOp	13 math math: toDescentDataFunctor_obj, descentDataEquivalence_inverse, comp_hom, isoMk_inv_hom, comp_hom_assoc, isoMk_hom_hom, toDescentDataFunctor_map_hom, descentDataEquivalence_unitIso, descentDataEquivalence_functor, fromDescentDataFunctor_map_hom, descentDataEquivalence_counitIso, fromDescentDataFunctor_obj, id_hom
instQuiver 📖	CompOp	—
isoMk 📖	CompOp	3 math math: isoMk_inv_hom, isoMk_hom_hom, descentDataEquivalence_unitIso
obj 📖	CompOp	23 math math: comm, comp_pullHom', instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, comp_hom, isoMk_inv_hom, comp_hom_assoc, isoMk_hom_hom, ofDescentData_obj, Hom.comm, descentDataEquivalence_unitIso, pullHom'_hom_self, Hom.comm_assoc, pullHom'_eq_hom, pullHom'_hom_comp, comm_assoc, pullHom'_self, descentData_hom, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom, comp_pullHom'_assoc, pullHom'_hom_comp_assoc, id_hom, pullHom'_ofDescentData_hom, descentData_obj
ofDescentData 📖	CompOp	5 math math: ofDescentData_hom, ofDescentData_obj, fromDescentDataFunctor_map_hom, fromDescentDataFunctor_obj, pullHom'_ofDescentData_hom
pullHom' 📖	CompOp	26 math math: comm, pullHom_pullHom', comp_pullHom', pullHom'_eq_pullHom_assoc, pullHom'_self', pullHom'₁₂_eq_pullHom_of_chosenPullback₃, comp_pullHom'', pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, pullHom'₁₃_eq_pullHom_of_chosenPullback₃, pullHom'₂₃_eq_pullHom_of_chosenPullback₃, pullHom'_eq_pullHom, pullHom'_p₁_p₂, pullHom'_hom_self, pullHom'_eq_hom, pullHom'_hom_comp, comm_assoc, pullHom'_self, descentData_hom, comp_pullHom''_assoc, pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, pullHom_pullHom'_assoc, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom, comp_pullHom'_assoc, pullHom'_hom_comp_assoc, pullHom'_ofDescentData_hom
toDescentDataFunctor 📖	CompOp	5 math math: toDescentDataFunctor_obj, toDescentDataFunctor_map_hom, descentDataEquivalence_unitIso, descentDataEquivalence_functor, descentDataEquivalence_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj CategoryTheory.Functor.map Hom.hom pullHom' hom	—	CategoryTheory.IsPullback.exists_lift CategoryTheory.Limits.ChosenPullback.isPullback CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.hp₂ CategoryTheory.Category.assoc pullHom_pullHom' pullHom'_p₁_p₂ CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.map_comp_assoc Hom.comm CategoryTheory.Pseudofunctor.mapComp'_inv_naturality
comm_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj CategoryTheory.Functor.map Hom.hom pullHom' hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.DescentData' CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj Hom.hom CategoryTheory.Pseudofunctor.DescentData' instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
comp_pullHom' 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj pullHom' hom	—	comp_pullHom'' pullHom'_hom_comp
comp_pullHom'' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₁ CategoryTheory.Limits.ChosenPullback₃.p₂ CategoryTheory.Limits.ChosenPullback₃.p₃ pullHom' CategoryTheory.Limits.ChosenPullback₃.p	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op pullHom'	—	CategoryTheory.Limits.ChosenPullback₃.exists_lift CategoryTheory.Limits.ChosenPullback₃.w₁ CategoryTheory.Limits.ChosenPullback₃.w₂ CategoryTheory.Category.assoc pullHom_pullHom'_assoc CategoryTheory.Limits.ChosenPullback₃.w₃ pullHom_pullHom' CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc
comp_pullHom''_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₁ CategoryTheory.Limits.ChosenPullback₃.p₂ CategoryTheory.Limits.ChosenPullback₃.p₃ pullHom' CategoryTheory.Limits.ChosenPullback₃.p	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op pullHom'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_pullHom''
comp_pullHom'_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj pullHom' hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_pullHom'
descentDataEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Pseudofunctor.DescentData' CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.DescentData.instCategory descentDataEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp fromDescentDataFunctor toDescentDataFunctor CategoryTheory.Functor.id CategoryTheory.Pseudofunctor.DescentData.isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.refl CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData.obj	—	—
descentDataEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Pseudofunctor.DescentData' CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.DescentData.instCategory descentDataEquivalence toDescentDataFunctor	—	—
descentDataEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Pseudofunctor.DescentData' CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.DescentData.instCategory descentDataEquivalence fromDescentDataFunctor	—	—
descentDataEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Pseudofunctor.DescentData' CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.DescentData.instCategory descentDataEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp toDescentDataFunctor fromDescentDataFunctor isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.refl CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
descentData_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Pseudofunctor.DescentData.hom descentData pullHom' obj hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
descentData_obj 📖	mathematical	—	CategoryTheory.Pseudofunctor.DescentData.obj descentData obj	—	—
fromDescentDataFunctor_map_hom 📖	mathematical	—	Hom.hom ofDescentData CategoryTheory.Functor.map CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Pseudofunctor.DescentData.instCategory CategoryTheory.Pseudofunctor.DescentData' instCategory fromDescentDataFunctor CategoryTheory.Pseudofunctor.DescentData.Hom.hom	—	—
fromDescentDataFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Pseudofunctor.DescentData.instCategory CategoryTheory.Pseudofunctor.DescentData' instCategory fromDescentDataFunctor ofDescentData	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Pseudofunctor.DescentData' CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj pullHom' hom	—	comp_pullHom' pullHom'_self
instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback.p₁ obj CategoryTheory.Limits.ChosenPullback.p₂ hom	—	CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.hp₂ pullHom'_p₁_p₂ instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom
isoMk_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.hom CategoryTheory.Pseudofunctor.DescentData' instCategory isoMk CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
isoMk_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.DescentData' instCategory isoMk CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
ofDescentData_hom 📖	mathematical	—	hom ofDescentData CategoryTheory.Pseudofunctor.DescentData.hom CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂	—	—
ofDescentData_obj 📖	mathematical	—	obj ofDescentData CategoryTheory.Pseudofunctor.DescentData.obj	—	—
pullHom'_eq_hom 📖	mathematical	—	pullHom' obj hom CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁	—	CategoryTheory.Limits.ChosenPullback.hp₂ pullHom'.congr_simp pullHom'_p₁_p₂
pullHom'_eq_pullHom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂	pullHom' CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂	—	CategoryTheory.Limits.ChosenPullback.isPullback CategoryTheory.IsPullback.hom_ext CategoryTheory.IsPullback.lift_fst CategoryTheory.IsPullback.lift_snd
pullHom'_eq_pullHom_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op pullHom' CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂	—	Mathlib.Tactic.Reassoc.eq_whisker' pullHom'_eq_pullHom
pullHom'_hom_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₁ obj CategoryTheory.Limits.ChosenPullback₃.p₂ CategoryTheory.Limits.ChosenPullback₃.p₃ pullHom' hom CategoryTheory.Limits.ChosenPullback₃.p	—	—
pullHom'_hom_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₁ obj CategoryTheory.Limits.ChosenPullback₃.p₂ pullHom' hom CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Limits.ChosenPullback₃.p₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullHom'_hom_comp
pullHom'_hom_self 📖	mathematical	—	pullHom' obj hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op	—	—
pullHom'_ofDescentData_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullHom' obj ofDescentData hom CategoryTheory.Pseudofunctor.DescentData.hom	—	CategoryTheory.IsPullback.exists_lift CategoryTheory.Limits.ChosenPullback.isPullback CategoryTheory.Category.assoc CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.hp₂ pullHom'_eq_pullHom Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Pseudofunctor.DescentData.pullHom_hom
pullHom'_p₁_p₂ 📖	mathematical	—	pullHom' CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂	—	CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.hp₂ CategoryTheory.Category.id_comp pullHom'_eq_pullHom CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_id
pullHom'_self 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	pullHom' obj hom CategoryTheory.CategoryStruct.id CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op	—	pullHom'_self' pullHom'_hom_self
pullHom'_self' 📖	mathematical	pullHom' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.comp	pullHom' CategoryTheory.CategoryStruct.id CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id pullHom_pullHom' CategoryTheory.Functor.map_id CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app
pullHom'₁₂_eq_pullHom_of_chosenPullback₃ 📖	mathematical	—	pullHom' CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Limits.ChosenPullback₃.p₁ CategoryTheory.Limits.ChosenPullback₃.p₂ CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback₃.pullback CategoryTheory.Limits.ChosenPullback₃.p₁₂	—	pullHom'_eq_pullHom CategoryTheory.Limits.ChosenPullback₃.w₁ CategoryTheory.Limits.ChosenPullback₃.w₂ CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁ CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂
pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₁ CategoryTheory.Limits.ChosenPullback₃.p₂ pullHom' CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback₃.pullback CategoryTheory.Limits.ChosenPullback₃.p₁₂	—	Mathlib.Tactic.Reassoc.eq_whisker' pullHom'₁₂_eq_pullHom_of_chosenPullback₃
pullHom'₁₃_eq_pullHom_of_chosenPullback₃ 📖	mathematical	—	pullHom' CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Limits.ChosenPullback₃.p₁ CategoryTheory.Limits.ChosenPullback₃.p₃ CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback₃.pullback CategoryTheory.Limits.ChosenPullback₃.p₁₃	—	pullHom'_eq_pullHom CategoryTheory.Limits.ChosenPullback₃.w₁ CategoryTheory.Limits.ChosenPullback₃.w₃ CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁ CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃
pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₁ CategoryTheory.Limits.ChosenPullback₃.p₃ pullHom' CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback₃.pullback CategoryTheory.Limits.ChosenPullback₃.p₁₃	—	Mathlib.Tactic.Reassoc.eq_whisker' pullHom'₁₃_eq_pullHom_of_chosenPullback₃
pullHom'₂₃_eq_pullHom_of_chosenPullback₃ 📖	mathematical	—	pullHom' CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Limits.ChosenPullback₃.p₂ CategoryTheory.Limits.ChosenPullback₃.p₃ CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback₃.pullback CategoryTheory.Limits.ChosenPullback₃.p₂₃	—	pullHom'_eq_pullHom CategoryTheory.Limits.ChosenPullback₃.w₂ CategoryTheory.Limits.ChosenPullback₃.w₃ CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂ CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃
pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback₃.chosenPullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback₃.p₂ CategoryTheory.Limits.ChosenPullback₃.p₃ pullHom' CategoryTheory.Limits.ChosenPullback₃.p CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom CategoryTheory.Limits.ChosenPullback₃.pullback CategoryTheory.Limits.ChosenPullback₃.p₂₃	—	Mathlib.Tactic.Reassoc.eq_whisker' pullHom'₂₃_eq_pullHom_of_chosenPullback₃
pullHom_pullHom' 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom pullHom'	—	CategoryTheory.Limits.ChosenPullback.isPullback CategoryTheory.IsPullback.lift_fst CategoryTheory.IsPullback.lift_snd pullHom'_eq_pullHom CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.locallyDiscreteBicategory.strict Quiver.Hom.comp_toLoc CategoryTheory.op_comp CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc
pullHom_pullHom'_assoc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom pullHom'	—	Mathlib.Tactic.Reassoc.eq_whisker' pullHom_pullHom'
toDescentDataFunctor_map_hom 📖	mathematical	—	CategoryTheory.Pseudofunctor.DescentData.Hom.hom descentData CategoryTheory.Functor.map CategoryTheory.Pseudofunctor.DescentData' instCategory CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Pseudofunctor.DescentData.instCategory toDescentDataFunctor Hom.hom	—	—
toDescentDataFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData' instCategory CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Pseudofunctor.DescentData.instCategory toDescentDataFunctor descentData	—	—

CategoryTheory.Pseudofunctor.DescentData'.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	13 math math: CategoryTheory.Pseudofunctor.DescentData'.comm, CategoryTheory.Pseudofunctor.DescentData'.comp_hom, CategoryTheory.Pseudofunctor.DescentData'.isoMk_inv_hom, ext_iff, CategoryTheory.Pseudofunctor.DescentData'.comp_hom_assoc, CategoryTheory.Pseudofunctor.DescentData'.hom_ext_iff, CategoryTheory.Pseudofunctor.DescentData'.isoMk_hom_hom, CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor_map_hom, comm, comm_assoc, CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor_map_hom, CategoryTheory.Pseudofunctor.DescentData'.comm_assoc, CategoryTheory.Pseudofunctor.DescentData'.id_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Pseudofunctor.DescentData'.obj CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Functor.map hom CategoryTheory.Pseudofunctor.DescentData'.hom	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Pseudofunctor.DescentData'.obj CategoryTheory.Functor.map hom CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Pseudofunctor.DescentData'.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext

---

← Back to Index