Documentation Verification Report

LocallyDiscrete

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

Statistics

Metric	Count
Definitions `IsLocallyDiscrete`, `LocallyDiscrete`, `as`, `categoryStruct`, `homSmallCategory`, `instDecidableEq`, `instInhabited`, `locallyDiscreteEquiv`, `locallyDiscreteBicategory`, `toLoc`	10
Theorems `instIsLocallyDiscreteLocallyDiscrete`, `instStrictOfIsLocallyDiscrete`, `toLoc`, `comp_as`, `eqToHom_toLoc`, `eq_of_hom`, `ext`, `ext_iff`, `id_as`, `locallyDiscreteEquiv_apply`, `locallyDiscreteEquiv_symm_apply_as`, `mk_as`, `subsingleton2Hom`, `strict`, `comp_toLoc`, `id_toLoc`, `toLoc_as`	17
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
`LocallyDiscrete` 📖	CompData	201 math math: `Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le`, `Pseudofunctor.DescentData.ofObj_hom`, `Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj`, `Pseudofunctor.DescentData'.comm`, `Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom`, `Pseudofunctor.isEquivalence_toDescentData`, `Pseudofunctor.DescentData'.comp_pullHom'`, `Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc`, `Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom`, `Pseudofunctor.DescentDataAsCoalgebra.counit`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom`, `Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.map_comp_eq`, `LocallyDiscrete.id_as`, `Pseudofunctor.DescentData.pullFunctor_map_hom`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app`, `LocallyDiscrete.comp_as`, `Pseudofunctor.DescentData.isoMk_inv_hom`, `Pseudofunctor.CoGrothendieck.map_map_base`, `Pseudofunctor.CoGrothendieck.map_map_fiber`, `Pseudofunctor.DescentData'.pullHom'_self'`, `Pseudofunctor.Grothendieck.map_id_eq`, `Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l`, `Pseudofunctor.DescentData.comp_hom`, `LocallyDiscrete.subsingleton2Hom`, `Pseudofunctor.Grothendieck.ext_iff`, `Functor.toOplaxFunctor'_obj`, `Pseudofunctor.toDescentDataAsCoalgebra_obj_obj`, `Pseudofunctor.isStackFor_ofArrows_iff`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom`, `Pseudofunctor.DescentData.iso_hom`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj`, `Bicategory.instIsLocallyDiscreteLocallyDiscrete`, `Pseudofunctor.DescentDataAsCoalgebra.coassoc_assoc`, `Pseudofunctor.presheafHom_obj`, `Pseudofunctor.DescentData'.comp_hom`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `Pseudofunctor.DescentData'.isoMk_inv_hom`, `Pseudofunctor.DescentData.iso_inv`, `Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CommSq.toLoc`, `Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app`, `Pseudofunctor.Grothendieck.map_id_map`, `Functor.toOplaxFunctor_obj`, `Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom`, `Pseudofunctor.toDescentDataAsCoalgebra_map_hom`, `Functor.toPseudofunctor_obj`, `Pseudofunctor.CoGrothendieck.ι_map_base`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_map`, `Pseudofunctor.DescentData'.comp_pullHom''`, `Pseudofunctor.isPrestackFor_ofArrows_iff`, `Pseudofunctor.DescentDataAsCoalgebra.Hom.comm`, `Pseudofunctor.CoGrothendieck.map_obj_fiber`, `Pseudofunctor.DescentData.Hom.comm_assoc`, `Pseudofunctor.Grothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.Hom.congr`, `FreeBicategory.preinclusion_map₂`, `Quiver.Hom.comp_toLoc`, `LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl`, `Pseudofunctor.DescentData'.comp_hom_assoc`, `Pseudofunctor.toDescentDataAsCoalgebra_obj_hom`, `Pseudofunctor.DescentData.ofObj_obj`, `Functor.toPseudofunctor_mapId`, `GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app`, `Pseudofunctor.CoGrothendieck.ext_iff`, `Pseudofunctor.DescentData.hom_comp_assoc`, `Pseudofunctor.Grothendieck.map_obj_fiber`, `Pseudofunctor.CoGrothendieck.ι_obj_fiber`, `Pseudofunctor.isStackFor_iff`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_map`, `Pseudofunctor.bijective_toDescentData_map_iff`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr`, `Pseudofunctor.CoGrothendieck.ι_map_fiber`, `Functor.toOplaxFunctor'_map`, `Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `LocallyDiscrete.mkPseudofunctor_map`, `Pseudofunctor.DescentData.pullFunctorObj_obj`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_obj`, `Functor.toOplaxFunctor_mapComp`, `LocallyDiscrete.mkPseudofunctor_mapId`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f`, `RingCat.moduleCatRestrictScalarsPseudofunctor_map`, `Pseudofunctor.DescentData'.isoMk_hom_hom`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj`, `Pseudofunctor.IsStack.essSurj_of_sieve`, `Functor.toPseudofunctor'_map`, `Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `FreeBicategory.normalize_naturality`, `LocallyDiscrete.mkPseudofunctor_mapComp`, `Pseudofunctor.toDescentData_obj`, `Pseudofunctor.DescentDataAsCoalgebra.id_hom`, `Functor.toPseudofunctor'_obj`, `LocallyDiscrete.eqToHom_toLoc`, `Functor.toOplaxFunctor_map`, `Pseudofunctor.presheafHomObjHomEquiv_apply`, `Pseudofunctor.DescentData'.Hom.comm`, `Pseudofunctor.Grothendieck.Hom.ext_iff`, `LocallyDiscrete.locallyDiscreteEquiv_apply`, `Functor.toPseudofunctor'_mapId`, `Pseudofunctor.isPrestackFor_iff`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom`, `Pseudofunctor.IsStackFor.isEquivalence`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj`, `Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `RingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `Pseudofunctor.Grothendieck.Hom.congr`, `Pseudofunctor.Grothendieck.map_comp_eq`, `Pseudofunctor.Grothendieck.map_map_fiber`, `Pseudofunctor.DescentData'.descentDataEquivalence_unitIso`, `Pseudofunctor.CoGrothendieck.ι_obj_base`, `Pseudofunctor.toDescentData_map_hom`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Pseudofunctor.DescentData'.pullHom'_hom_self`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `Pseudofunctor.DescentData'.Hom.comm_assoc`, `locallyDiscreteBicategory.strict`, `Pseudofunctor.DescentDataAsCoalgebra.comp_hom_assoc`, `Pseudofunctor.IsStackFor.essSurj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `Pseudofunctor.DescentData'.pullHom'_hom_comp`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp`, `Pseudofunctor.DescentData'.comm_assoc`, `Pseudofunctor.DescentData'.pullHom'_self`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl`, `Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq`, `LocallyDiscrete.mkPseudofunctor_obj`, `Functor.toPseudofunctor'_mapComp`, `Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom`, `Quiver.Hom.id_toLoc`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc`, `Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq`, `Pseudofunctor.CoGrothendieck.comp_const`, `Pseudofunctor.CoGrothendieck.map_id_eq`, `Pseudofunctor.CoGrothendieck.compIso_inv_app`, `Functor.toOplaxFunctor_mapId`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app`, `Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom`, `Pseudofunctor.DescentDataAsCoalgebra.coassoc`, `GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom`, `Pseudofunctor.DescentData.id_hom`, `Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom`, `Pseudofunctor.DescentData.isoMk_hom_hom`, `Pseudofunctor.DescentDataAsCoalgebra.isoMk_inv_hom`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq`, `Pseudofunctor.DescentDataAsCoalgebra.Hom.comm_assoc`, `Pseudofunctor.DescentData.hom_self`, `Pseudofunctor.DescentData.comp_hom_assoc`, `Functor.toOplaxFunctor'_mapComp`, `Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `Pseudofunctor.DescentData'.comp_pullHom''_assoc`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId`, `Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r`, `Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `FreeBicategory.preinclusion_obj`, `Pseudofunctor.CoGrothendieck.map_id_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr`, `Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc`, `Pseudofunctor.DescentData'.pullHom_pullHom'_assoc`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map`, `Pseudofunctor.DescentData'.descentDataEquivalence_counitIso`, `Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A`, `Pseudofunctor.DescentData'.comp_pullHom'_assoc`, `Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl`, `Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `Pseudofunctor.DescentData'.id_hom`, `Pseudofunctor.CoGrothendieck.compIso_hom_app`, `Pseudofunctor.DescentData.hom_comp`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app`, `Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr`, `Pseudofunctor.CoGrothendieck.Hom.ext_iff`, `Functor.toPseudofunctor_mapComp`, `Pseudofunctor.Grothendieck.map_map_base`, `Functor.toPseudofunctor_map`, `Functor.toOplaxFunctor'_mapId`, `Pseudofunctor.DescentDataAsCoalgebra.counit_assoc`, `Pseudofunctor.DescentDataAsCoalgebra.isoMk_hom_hom`, `GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app`, `Pseudofunctor.DescentDataAsCoalgebra.comp_hom`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f`, `Pseudofunctor.DescentData.Hom.comm`
`locallyDiscreteBicategory` 📖	CompOp	193 math math: `Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le`, `Pseudofunctor.DescentData.ofObj_hom`, `Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj`, `Pseudofunctor.DescentData'.comm`, `Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom`, `Pseudofunctor.isEquivalence_toDescentData`, `Pseudofunctor.DescentData'.comp_pullHom'`, `Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc`, `Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom`, `Pseudofunctor.DescentDataAsCoalgebra.counit`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom`, `Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.map_comp_eq`, `Pseudofunctor.DescentData.pullFunctor_map_hom`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app`, `Pseudofunctor.DescentData.isoMk_inv_hom`, `Pseudofunctor.CoGrothendieck.map_map_base`, `Pseudofunctor.CoGrothendieck.map_map_fiber`, `Pseudofunctor.DescentData'.pullHom'_self'`, `Pseudofunctor.Grothendieck.map_id_eq`, `Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l`, `Pseudofunctor.DescentData.comp_hom`, `Pseudofunctor.Grothendieck.ext_iff`, `Functor.toOplaxFunctor'_obj`, `Pseudofunctor.toDescentDataAsCoalgebra_obj_obj`, `Pseudofunctor.isStackFor_ofArrows_iff`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom`, `Pseudofunctor.DescentData.iso_hom`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj`, `Bicategory.instIsLocallyDiscreteLocallyDiscrete`, `Pseudofunctor.DescentDataAsCoalgebra.coassoc_assoc`, `Pseudofunctor.presheafHom_obj`, `Pseudofunctor.DescentData'.comp_hom`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `Pseudofunctor.DescentData'.isoMk_inv_hom`, `Pseudofunctor.DescentData.iso_inv`, `Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CommSq.toLoc`, `Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app`, `Pseudofunctor.Grothendieck.map_id_map`, `Functor.toOplaxFunctor_obj`, `Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom`, `Pseudofunctor.toDescentDataAsCoalgebra_map_hom`, `Functor.toPseudofunctor_obj`, `Pseudofunctor.CoGrothendieck.ι_map_base`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_map`, `Pseudofunctor.DescentData'.comp_pullHom''`, `Pseudofunctor.isPrestackFor_ofArrows_iff`, `Pseudofunctor.DescentDataAsCoalgebra.Hom.comm`, `Pseudofunctor.CoGrothendieck.map_obj_fiber`, `Pseudofunctor.DescentData.Hom.comm_assoc`, `Pseudofunctor.Grothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.Hom.congr`, `FreeBicategory.preinclusion_map₂`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl`, `Pseudofunctor.DescentData'.comp_hom_assoc`, `Pseudofunctor.toDescentDataAsCoalgebra_obj_hom`, `Pseudofunctor.DescentData.ofObj_obj`, `Functor.toPseudofunctor_mapId`, `GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app`, `Pseudofunctor.CoGrothendieck.ext_iff`, `Pseudofunctor.DescentData.hom_comp_assoc`, `Pseudofunctor.Grothendieck.map_obj_fiber`, `Pseudofunctor.CoGrothendieck.ι_obj_fiber`, `Pseudofunctor.isStackFor_iff`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_map`, `Pseudofunctor.bijective_toDescentData_map_iff`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr`, `Pseudofunctor.CoGrothendieck.ι_map_fiber`, `Functor.toOplaxFunctor'_map`, `Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `LocallyDiscrete.mkPseudofunctor_map`, `Pseudofunctor.DescentData.pullFunctorObj_obj`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_obj`, `Functor.toOplaxFunctor_mapComp`, `LocallyDiscrete.mkPseudofunctor_mapId`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f`, `RingCat.moduleCatRestrictScalarsPseudofunctor_map`, `Pseudofunctor.DescentData'.isoMk_hom_hom`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj`, `Pseudofunctor.IsStack.essSurj_of_sieve`, `Functor.toPseudofunctor'_map`, `Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `FreeBicategory.normalize_naturality`, `LocallyDiscrete.mkPseudofunctor_mapComp`, `Pseudofunctor.toDescentData_obj`, `Pseudofunctor.DescentDataAsCoalgebra.id_hom`, `Functor.toPseudofunctor'_obj`, `Functor.toOplaxFunctor_map`, `Pseudofunctor.presheafHomObjHomEquiv_apply`, `Pseudofunctor.DescentData'.Hom.comm`, `Pseudofunctor.Grothendieck.Hom.ext_iff`, `Functor.toPseudofunctor'_mapId`, `Pseudofunctor.isPrestackFor_iff`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom`, `Pseudofunctor.IsStackFor.isEquivalence`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj`, `Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `RingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `Pseudofunctor.Grothendieck.Hom.congr`, `Pseudofunctor.Grothendieck.map_comp_eq`, `Pseudofunctor.Grothendieck.map_map_fiber`, `Pseudofunctor.DescentData'.descentDataEquivalence_unitIso`, `Pseudofunctor.CoGrothendieck.ι_obj_base`, `Pseudofunctor.toDescentData_map_hom`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Pseudofunctor.DescentData'.pullHom'_hom_self`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `Pseudofunctor.DescentData'.Hom.comm_assoc`, `locallyDiscreteBicategory.strict`, `Pseudofunctor.DescentDataAsCoalgebra.comp_hom_assoc`, `Pseudofunctor.IsStackFor.essSurj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `Pseudofunctor.DescentData'.pullHom'_hom_comp`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp`, `Pseudofunctor.DescentData'.comm_assoc`, `Pseudofunctor.DescentData'.pullHom'_self`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl`, `Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq`, `LocallyDiscrete.mkPseudofunctor_obj`, `Functor.toPseudofunctor'_mapComp`, `Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc`, `Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq`, `Pseudofunctor.CoGrothendieck.comp_const`, `Pseudofunctor.CoGrothendieck.map_id_eq`, `Pseudofunctor.CoGrothendieck.compIso_inv_app`, `Functor.toOplaxFunctor_mapId`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app`, `Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom`, `Pseudofunctor.DescentDataAsCoalgebra.coassoc`, `GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom`, `Pseudofunctor.DescentData.id_hom`, `Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom`, `Pseudofunctor.DescentData.isoMk_hom_hom`, `Pseudofunctor.DescentDataAsCoalgebra.isoMk_inv_hom`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq`, `Pseudofunctor.DescentDataAsCoalgebra.Hom.comm_assoc`, `Pseudofunctor.DescentData.hom_self`, `Pseudofunctor.DescentData.comp_hom_assoc`, `Functor.toOplaxFunctor'_mapComp`, `Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `Pseudofunctor.DescentData'.comp_pullHom''_assoc`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId`, `Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r`, `Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `FreeBicategory.preinclusion_obj`, `Pseudofunctor.CoGrothendieck.map_id_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr`, `Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc`, `Pseudofunctor.DescentData'.pullHom_pullHom'_assoc`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map`, `Pseudofunctor.DescentData'.descentDataEquivalence_counitIso`, `Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A`, `Pseudofunctor.DescentData'.comp_pullHom'_assoc`, `Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl`, `Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `Pseudofunctor.DescentData'.id_hom`, `Pseudofunctor.CoGrothendieck.compIso_hom_app`, `Pseudofunctor.DescentData.hom_comp`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app`, `Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr`, `Pseudofunctor.CoGrothendieck.Hom.ext_iff`, `Functor.toPseudofunctor_mapComp`, `Pseudofunctor.Grothendieck.map_map_base`, `Functor.toPseudofunctor_map`, `Functor.toOplaxFunctor'_mapId`, `Pseudofunctor.DescentDataAsCoalgebra.counit_assoc`, `Pseudofunctor.DescentDataAsCoalgebra.isoMk_hom_hom`, `GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app`, `Pseudofunctor.DescentDataAsCoalgebra.comp_hom`, `Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f`, `Pseudofunctor.DescentData.Hom.comm`

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`IsLocallyDiscrete` 📖	MathDef	1 math math: `instIsLocallyDiscreteLocallyDiscrete`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocallyDiscreteLocallyDiscrete` 📖	mathematical	—	`IsLocallyDiscrete` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory`	—	`CategoryTheory.Discrete.isDiscrete`
`instStrictOfIsLocallyDiscrete` 📖	mathematical	`IsLocallyDiscrete`	`Strict`	—	`CategoryTheory.obj_ext_of_isDiscrete` `CategoryTheory.Iso.ext` `CategoryTheory.IsDiscrete.subsingleton`

CategoryTheory.CommSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toLoc` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CommSq` `CategoryTheory.LocallyDiscrete` `CategoryTheory.StrictBicategory.category` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.locallyDiscreteBicategory.strict` `Quiver.Hom.toLoc` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.locallyDiscreteBicategory.strict` `w`

CategoryTheory.LocallyDiscrete

Definitions

Name	Category	Theorems
`as` 📖	CompOp	63 math math: `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `mk_as`, `id_as`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app`, `comp_as`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l`, `CategoryTheory.Functor.toOplaxFunctor'_obj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app`, `CategoryTheory.Functor.toOplaxFunctor_obj`, `CategoryTheory.Functor.toPseudofunctor_obj`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_map`, `locallyDiscreteEquiv_symm_apply_as`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl`, `CategoryTheory.Functor.toPseudofunctor_mapId`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr`, `CategoryTheory.Functor.toOplaxFunctor'_map`, `ext_iff`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `mkPseudofunctor_map`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_obj`, `CategoryTheory.Functor.toOplaxFunctor_mapComp`, `mkPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr`, `RingCat.moduleCatRestrictScalarsPseudofunctor_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj`, `CategoryTheory.Functor.toPseudofunctor'_map`, `CategoryTheory.FreeBicategory.normalize_naturality`, `mkPseudofunctor_mapComp`, `CategoryTheory.Functor.toPseudofunctor'_obj`, `CategoryTheory.Functor.toOplaxFunctor_map`, `locallyDiscreteEquiv_apply`, `CategoryTheory.Functor.toPseudofunctor'_mapId`, `RingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl`, `mkPseudofunctor_obj`, `CategoryTheory.Functor.toPseudofunctor'_mapComp`, `CategoryTheory.Functor.toOplaxFunctor_mapId`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl`, `CategoryTheory.Functor.toOplaxFunctor'_mapComp`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr`, `Quiver.Hom.toLoc_as`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr`, `CategoryTheory.Functor.toPseudofunctor_mapComp`, `CategoryTheory.Functor.toPseudofunctor_map`, `CategoryTheory.Functor.toOplaxFunctor'_mapId`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app`
`categoryStruct` 📖	CompOp	10 math math: `id_as`, `comp_as`, `subsingleton2Hom`, `Quiver.Hom.comp_toLoc`, `eqToHom_toLoc`, `CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply`, `Quiver.Hom.id_toLoc`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`
`homSmallCategory` 📖	CompOp	1 math math: `subsingleton2Hom`
`instDecidableEq` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`locallyDiscreteEquiv` 📖	CompOp	2 math math: `locallyDiscreteEquiv_symm_apply_as`, `locallyDiscreteEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `as` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LocallyDiscrete` `categoryStruct`	—	—
`eqToHom_toLoc` 📖	mathematical	—	`Quiver.Hom.toLoc` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom` `CategoryTheory.LocallyDiscrete` `categoryStruct`	—	—
`eq_of_hom` 📖	—	—	—	—	`CategoryTheory.Discrete.ext`
`ext` 📖	—	`as`	—	—	—
`ext_iff` 📖	mathematical	—	`as`	—	`ext`
`id_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `as` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LocallyDiscrete` `categoryStruct`	—	—
`locallyDiscreteEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.LocallyDiscrete` `EquivLike.toFunLike` `Equiv.instEquivLike` `locallyDiscreteEquiv` `as`	—	—
`locallyDiscreteEquiv_symm_apply_as` 📖	mathematical	—	`as` `DFunLike.coe` `Equiv` `CategoryTheory.LocallyDiscrete` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `locallyDiscreteEquiv`	—	—
`mk_as` 📖	mathematical	—	`as`	—	—
`subsingleton2Hom` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.LocallyDiscrete` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `homSmallCategory`	—	`CategoryTheory.Discrete.instSubsingletonDiscreteHom`

CategoryTheory.locallyDiscreteBicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strict` 📖	mathematical	—	`CategoryTheory.Bicategory.Strict` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory`	—	`CategoryTheory.Discrete.ext` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`

Quiver.Hom

Definitions

Name	Category	Theorems
`toLoc` 📖	CompOp	82 math math: `CategoryTheory.Pseudofunctor.DescentData.ofObj_hom`, `CategoryTheory.Pseudofunctor.DescentData'.comm`, `CategoryTheory.Pseudofunctor.isEquivalence_toDescentDataAsCoalgebra_iff_isEquivalence_comonadComparison`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom`, `CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self'`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_obj`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom`, `CategoryTheory.Pseudofunctor.DescentData.iso_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc_assoc`, `CategoryTheory.Pseudofunctor.presheafHom_obj`, `CategoryTheory.Pseudofunctor.DescentData.iso_inv`, `CategoryTheory.CommSq.toLoc`, `CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_map_hom`, `CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom''`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm`, `CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc`, `CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr`, `comp_toLoc`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_hom`, `CategoryTheory.Pseudofunctor.DescentData.ofObj_obj`, `CategoryTheory.Functor.toPseudofunctor_mapId`, `CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc`, `CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj`, `CategoryTheory.Functor.toOplaxFunctor_mapComp`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_a`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f`, `CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f`, `CategoryTheory.LocallyDiscrete.eqToHom_toLoc`, `CategoryTheory.Functor.toOplaxFunctor_map`, `CategoryTheory.Pseudofunctor.DescentData'.Hom.comm`, `CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj`, `CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr`, `CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.toDescentData_map_hom`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_self`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.Hom.comm_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f`, `CategoryTheory.Pseudofunctor.DescentData'.comm_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self`, `id_toLoc`, `CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc`, `CategoryTheory.Functor.toOplaxFunctor_mapId`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc`, `CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm_assoc`, `CategoryTheory.Pseudofunctor.DescentData.hom_self`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom''_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc`, `toLoc_as`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom_pullHom'_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A`, `CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'_assoc`, `CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.DescentData.hom_comp`, `CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff`, `CategoryTheory.Functor.toPseudofunctor_mapComp`, `CategoryTheory.Functor.toPseudofunctor_map`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit_assoc`, `CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f`, `CategoryTheory.Pseudofunctor.DescentData.Hom.comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toLoc` 📖	mathematical	—	`toLoc` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LocallyDiscrete` `CategoryTheory.LocallyDiscrete.categoryStruct`	—	—
`id_toLoc` 📖	mathematical	—	`toLoc` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LocallyDiscrete` `CategoryTheory.LocallyDiscrete.categoryStruct`	—	—
`toLoc_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.LocallyDiscrete.as` `toLoc`	—	—

---

← Back to Index