Prefunctor

📁 Source: Mathlib/Combinatorics/Quiver/Prefunctor.lean

Statistics

Metric	Count
Definitions Prefunctor, comp, id, instInhabited, map, obj, «term_⋙q_», «term_⥤q_», «term𝟭q»	9
Theorems comp_assoc, comp_id, comp_map, comp_obj, congr_hom, congr_map, congr_obj, ext, ext', homOfEq_map, id_comp, id_map, id_obj, mk_map, mk_obj	15
Total	24

Prefunctor

Definitions

Name	Category	Theorems
comp 📖	CompOp	27 math math: CategoryTheory.PrelaxFunctorStruct.comp_toPrefunctor, CategoryTheory.Quiv.comp_eq_comp, comp_map, CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, Quiver.Symmetrify.lift_spec, CategoryTheory.Cat.freeMap_comp, comp_obj, Quiver.freeGroupoidFunctor_comp, comp_assoc, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, Quiver.SingleObj.toPrefunctor_comp, Quiver.FreeGroupoid.lift_spec, CategoryTheory.Functor.toPrefunctor_comp, IsCovering.comp, comp_id, CategoryTheory.Paths.lift_spec, CategoryTheory.Cat.freeMapCompIso_hom_app, costar_comp, Quiver.Push.lift_comp, CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor, Quiver.FreeGroupoid.of_eq, mapReverseComp, star_comp, Quiver.SingleObj.toPrefunctor_symm_comp, id_comp, mapPath_comp_apply, CategoryTheory.Cat.freeMapCompIso_inv_app
id 📖	CompOp	15 math math: CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, Quiver.SingleObj.toPrefunctor_symm_id, mapReverseId, id_obj, CategoryTheory.Cat.freeMapIdIso_hom_app, mapPath_id, comp_id, CategoryTheory.Cat.freeMap_id, Quiver.SingleObj.toPrefunctor_id, Quiver.freeGroupoidFunctor_id, id_map, id_comp, CategoryTheory.Quiv.id_eq_id, CategoryTheory.PrelaxFunctorStruct.id_toPrefunctor, CategoryTheory.Cat.freeMapIdIso_inv_app
instInhabited 📖	CompOp	—
map 📖	CompOp	634 math math: CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc, CategoryTheory.StrictPseudofunctorPreCore.map_id, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp', AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj, CategoryTheory.Pseudofunctor.map₂_associator_assoc, CategoryTheory.LaxFunctor.map₂_associator_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app_assoc, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_hom, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, CategoryTheory.Bicategory.Prod.snd_map, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.OplaxFunctor.map₂_associator, CategoryTheory.ReflPrefunctor.id_map, CategoryTheory.LaxFunctor.map₂_leftUnitor_assoc, CategoryTheory.Quiv.homEquivOfIso_symm_apply, comp_map, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, CategoryTheory.LaxFunctor.comp_mapId, CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.map₂_associator_app, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_inv, CategoryTheory.Functor.toPrefunctor_map, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.StrictPseudofunctorCore.map₂_associator, CategoryTheory.Pseudofunctor.map₂_left_unitor, CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.StrictPseudofunctor.mk''_mapId, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_isIso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, CategoryTheory.ReflQuiv.id_map, CategoryTheory.Cat.FreeRefl.lift_map, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, CategoryTheory.ReflQuiv.comp_map, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Pseudofunctor.mapComp_id_left, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app, CategoryTheory.StrictPseudofunctor.comp_mapComp_hom, CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.StrictPseudofunctor.comp_mapId_hom, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapComp, CategoryTheory.Bicategory.Prod.fst_mapComp_hom, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app, CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapId, CategoryTheory.Pseudofunctor.map₂_associator_app, Quiver.SingleObj.toPrefunctor_apply_map, CategoryTheory.Lax.OplaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp_id_right, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, homOfEq_map, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Oplax.LaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Oplax.StrongTrans.naturality_comp, CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc, CategoryTheory.Functor.toPseudoFunctor'_map, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.toLax_mapComp, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Lax.LaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.DescentData.iso_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Oplax.StrongTrans.id_naturality_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Quiv.homEquivOfIso_apply, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.Quiv.inv_map_hom_map_of_iso, CategoryTheory.Oplax.LaxTrans.id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality, CategoryTheory.StrictPseudofunctor.comp_mapId_inv, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.OplaxFunctor.map₂_associator_app_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapComp, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.LaxFunctor.map₂_associator_app_assoc, CategoryTheory.Lax.LaxTrans.id_naturality, Quiver.Symmetrify.lift_reverse, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, map_reverse, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app, CategoryTheory.Bicategory.InducedBicategory.forget_map, CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc, CategoryTheory.PrelaxFunctor.map₂_eqToHom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom, CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_map₂, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app, CategoryTheory.PrelaxFunctor.map₂_hom_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.ReflPrefunctor.congr_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId, CategoryTheory.Bicategory.Prod.swap_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, CategoryTheory.Paths.of_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, CategoryTheory.Functor.toPseudoFunctor_map, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, mapPath_toPath, CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.FreeBicategory.preinclusion_map₂, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv, CategoryTheory.OplaxFunctor.map₂_associator_assoc, Quiver.Symmetrify.of_map, CategoryTheory.Pseudofunctor.map₂_whisker_left, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_assoc, CategoryTheory.Lax.StrongTrans.toLax_naturality, CategoryTheory.ReflPrefunctor.congr_map, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapId, CategoryTheory.PrelaxFunctor.map₂_hom_inv_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.StrictlyUnitaryLaxFunctor.map_id, CategoryTheory.FreeBicategory.of_map, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, CategoryTheory.Lax.OplaxTrans.naturality_naturality, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', CategoryTheory.Bicategory.Prod.fst_mapId_hom, CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.StrictPseudofunctor.comp_map, CategoryTheory.PrelaxFunctor.map₂_inv, CategoryTheory.StrictPseudofunctorPreCore.map_comp, CategoryTheory.StrictPseudofunctor.mk''_map, CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Quiv.hom_map_inv_map_of_iso, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, MapReverse.map_reverse', CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc, CategoryTheory.StrictPseudofunctor.map_comp, CategoryTheory.Functor.toOplaxFunctor'_map, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv, CategoryTheory.Cat.toFreeRefl_map, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality, CategoryTheory.ReflPrefunctor.map_id, CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom, CategoryTheory.LocallyDiscrete.mkPseudofunctor_map, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc, CategoryTheory.Lax.OplaxTrans.id_naturality, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, CategoryTheory.OplaxFunctor.map₂_leftUnitor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.StrictPseudofunctor.mk'_map, CategoryTheory.Lax.LaxTrans.naturality_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.Lax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv, CategoryTheory.Pseudofunctor.toLax_mapId', CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.StrictlyUnitaryLaxFunctor.id_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, RingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.LaxFunctor.map₂_associator, CategoryTheory.OplaxFunctor.mapComp_id_right_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_hom, CategoryTheory.OplaxFunctor.mapComp_assoc_right, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_inv, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Paths.lift_cons, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, CategoryTheory.ReflPrefunctor.comp_map, CategoryTheory.Pseudofunctor.toLax_mapId, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom, CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_inv, CategoryTheory.OplaxFunctor.map₂_rightUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.Pseudofunctor.map₂_left_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.StrictPseudofunctor.toFunctor_map, CategoryTheory.Bicategory.Prod.snd_mapId_hom, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_hom, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_assoc, CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.FreeBicategory.normalize_naturality, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom, CategoryTheory.Bicategory.Prod.sectL_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id, CategoryTheory.OplaxFunctor.mapComp_id_right, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_hom, CategoryTheory.Pseudofunctor.mapComp_id_right_inv, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc, CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.id_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, CategoryTheory.Functor.toOplaxFunctor_map, CategoryTheory.Pseudofunctor.map₂_whisker_right, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, costar_apply, CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.LaxFunctor.map₂_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, CategoryTheory.Bicategory.Prod.snd_mapId_inv, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Lax.StrongTrans.naturality_naturality, CategoryTheory.Oplax.OplaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv, CategoryTheory.Pseudofunctor.map₂_right_unitor, CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.PrelaxFunctorStruct.comp_map₂, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.PrelaxFunctor.map₂_comp, CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.PrelaxFunctor.mapFunctor_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc, CategoryTheory.StrictPseudofunctor.comp_mapComp_inv, star_apply, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, mk_map, CategoryTheory.Lax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, congr_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.StrictPseudofunctor.id_map, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.map₂_associator, CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, Quiver.Push.of_reverse, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Bicategory.Prod.fst_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_assoc, CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp', CategoryTheory.Lax.StrongTrans.id_naturality_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_map, CategoryTheory.Lax.OplaxTrans.naturality_id, CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom, CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map, CategoryTheory.PrelaxFunctor.map₂_comp_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right, CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.PrelaxFunctor.map₂_isIso, CategoryTheory.LaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, CategoryTheory.StrictPseudofunctor.comp_map₂, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc, CategoryTheory.PrelaxFunctor.map₂_inv_hom_assoc, CategoryTheory.Bicategory.Prod.fst_mapComp_inv, CategoryTheory.Oplax.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom, mapPath_cons, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.map_id, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_left_app, costar_snd, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff, CategoryTheory.Bicategory.Prod.snd_mapComp_hom, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.PrelaxFunctor.map₂_id, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map, CategoryTheory.StrictPseudofunctor.mk''_mapComp, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality, CategoryTheory.Oplax.StrongTrans.id_naturality_hom, CategoryTheory.Paths.lift_toPath, CategoryTheory.LaxFunctor.mapComp_assoc_left, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_right, CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_map, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapComp, CategoryTheory.Oplax.StrongTrans.naturality_naturality, CategoryTheory.PrelaxFunctor.map₂Iso_hom, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.PrelaxFunctor.map₂Iso_inv, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.OplaxFunctor.mapComp_id_left_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapId, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Bicategory.Prod.swap_mapComp_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc, IsCovering.map_injective, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, id_map, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Cat.freeReflMap_map, CategoryTheory.Pseudofunctor.mapId'_hom_naturality, CategoryTheory.Pseudofunctor.DescentData.hom_self, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app, CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, SSet.OneTruncation₂.map_map, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, symmetrify_map, CategoryTheory.Oplax.StrongTrans.toOplax_naturality, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, congr_map, CategoryTheory.Pseudofunctor.comp_mapComp, star_snd, CategoryTheory.Bicategory.Prod.swap_mapComp_inv, CategoryTheory.PrelaxFunctor.map₂Iso_eqToIso, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp, CategoryTheory.Pseudofunctor.toOplax_mapId', CategoryTheory.Bicategory.Prod.snd_mapComp_inv, CategoryTheory.Pseudofunctor.map₂_whisker_right_app, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.ReflPrefunctor.mk_map, CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.LaxFunctor.comp_mapComp, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, Quiver.SingleObj.toPrefunctor_symm_apply, CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso_assoc, CategoryTheory.PrelaxFunctor.map₂_inv_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, CategoryTheory.Bicategory.Prod.swap_mapId_hom, CategoryTheory.LaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.toLax_mapComp', CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq, CategoryTheory.LaxFunctor.mapComp_naturality_left, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_inv, CategoryTheory.Pseudofunctor.comp_mapId, CategoryTheory.Bicategory.Prod.swap_mapId_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, CategoryTheory.Bicategory.Prod.sectR_map, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_inv, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.LaxFunctor.map₂_leftUnitor_app, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map₂, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv, CategoryTheory.Pseudofunctor.DescentData.hom_comp, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv, CategoryTheory.Pseudofunctor.whiskerRightIso_mapId, CategoryTheory.Pseudofunctor.toOplax_mapComp', CategoryTheory.LaxFunctor.map₂_leftUnitor_hom, CategoryTheory.Bicategory.Prod.fst_mapId_inv, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso, CategoryTheory.OplaxFunctor.mapComp_id_left, CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.LaxFunctor.map₂_rightUnitor, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map₂, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc
obj 📖	CompOp	771 math math: CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, CategoryTheory.Quiv.equivOfIso_symm_apply, CategoryTheory.StrictPseudofunctorPreCore.map_id, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp', CategoryTheory.Oplax.StrongTrans.Modification.vcomp_app, CategoryTheory.Pseudofunctor.map₂_associator_assoc, CategoryTheory.LaxFunctor.map₂_associator_assoc, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app_assoc, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_hom, CategoryTheory.FreeBicategory.lift_mapId, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.OplaxFunctor.map₂_associator, CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_assoc, CategoryTheory.Quiv.homEquivOfIso_symm_apply, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_obj, comp_map, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, CategoryTheory.ReflPrefunctor.id_obj, CategoryTheory.LaxFunctor.comp_mapId, CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.map₂_associator_app, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app, CategoryTheory.Oplax.OplaxTrans.Modification.vcomp_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.FreeBicategory.liftHom_id, CategoryTheory.Pseudofunctor.StrongTrans.comp_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, CategoryTheory.StrictPseudofunctor.mk'_obj, CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.homCategory_id_as_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_inv, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, CategoryTheory.Functor.toPseudoFunctor'_obj, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.StrictPseudofunctorCore.map₂_associator, CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom, CategoryTheory.Pseudofunctor.map₂_left_unitor, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base, CategoryTheory.Cat.freeReflMap_obj, CategoryTheory.StrictPseudofunctor.mk''_mapId, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_isIso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.Cat.freeMap_obj, CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.DescentData.comp_hom, CategoryTheory.ReflPrefunctor.congr_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_app, CategoryTheory.ReflQuiv.comp_map, CategoryTheory.StrictPseudofunctor.id_obj, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.StrongTrans.homCategory_id_as_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.Grothendieck.ext_iff, CategoryTheory.Lax.LaxTrans.id_app, CategoryTheory.StrictlyUnitaryLaxFunctor.id_obj, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Pseudofunctor.mapComp_id_left, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app, CategoryTheory.StrictPseudofunctor.comp_mapComp_hom, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, CategoryTheory.Functor.toOplaxFunctor'_obj, CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.StrictPseudofunctor.comp_mapId_hom, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapComp, CategoryTheory.Bicategory.Prod.fst_mapComp_hom, id_obj, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app, CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapId, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, CategoryTheory.Pseudofunctor.map₂_associator_app, CategoryTheory.Lax.OplaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp_id_right, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, homOfEq_map, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Oplax.LaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Oplax.StrongTrans.naturality_comp, CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc, CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, CategoryTheory.Cat.toFreeRefl_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.toLax_mapComp, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Lax.LaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.DescentData.iso_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Oplax.StrongTrans.id_naturality_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc, comp_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, CategoryTheory.Oplax.LaxTrans.id_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app, CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Quiv.homEquivOfIso_apply, CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc, IsCovering.star_bijective, CategoryTheory.Bicategory.Prod.sectL_obj, CategoryTheory.Quiv.lift_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.Quiv.inv_map_hom_map_of_iso, CategoryTheory.Oplax.LaxTrans.id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, mapPath_nil, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app, CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality, CategoryTheory.StrictPseudofunctor.comp_mapId_inv, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, star_fst, CategoryTheory.OplaxFunctor.map₂_associator_app_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapComp, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.LaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans, CategoryTheory.Lax.LaxTrans.id_naturality, Quiver.Symmetrify.lift_reverse, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, map_reverse, CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj, CategoryTheory.Functor.toOplaxFunctor_obj, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_obj, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_app, CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc, mk_obj, CategoryTheory.PrelaxFunctor.map₂_eqToHom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.Functor.toPrefunctor_obj, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app, CategoryTheory.PrelaxFunctor.map₂_hom_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.ReflPrefunctor.congr_hom, CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, Quiver.Symmetrify.of_obj, CategoryTheory.OplaxFunctor.mapComp_assoc_left, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Oplax.StrongTrans.Modification.id_app, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, CategoryTheory.Oplax.StrongTrans.isoMk_hom_as_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, mapPath_toPath, CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.FreeBicategory.preinclusion_map₂, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv, CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app, CategoryTheory.OplaxFunctor.map₂_associator_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_left, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_assoc, CategoryTheory.Lax.StrongTrans.toLax_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapId, CategoryTheory.PrelaxFunctor.map₂_hom_inv_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.StrictlyUnitaryLaxFunctor.map_id, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv, CategoryTheory.ReflQuiv.comp_obj, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ext_iff, CategoryTheory.Lax.OplaxTrans.naturality_naturality, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', CategoryTheory.Bicategory.Prod.fst_mapId_hom, CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.StrictPseudofunctor.comp_map, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_fiber, CategoryTheory.PrelaxFunctor.map₂_inv, CategoryTheory.StrictPseudofunctorPreCore.map_comp, CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.isStackFor_iff, CategoryTheory.Quiv.hom_map_inv_map_of_iso, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, MapReverse.map_reverse', CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.StrictPseudofunctor.toFunctor_obj, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc, CategoryTheory.StrictPseudofunctor.map_comp, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.id_obj, CategoryTheory.Cat.freeMapCompIso_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv, CategoryTheory.Oplax.OplaxTrans.homCategory_comp_as_app, CategoryTheory.Bicategory.Prod.snd_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality, CategoryTheory.ReflPrefunctor.map_id, CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc, CategoryTheory.Lax.OplaxTrans.id_naturality, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, CategoryTheory.PrelaxFunctor.mapFunctor_map, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, CategoryTheory.OplaxFunctor.map₂_leftUnitor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_obj, CategoryTheory.Lax.LaxTrans.naturality_naturality, Quiver.Push.of_obj, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, CategoryTheory.Quiv.lift_map, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.Lax.StrongTrans.naturality_id, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv, CategoryTheory.Pseudofunctor.toLax_mapId', CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.mapComp_id_left_inv, CategoryTheory.WithInitial.pseudofunctor_mapId, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, CategoryTheory.LaxFunctor.map₂_associator, CategoryTheory.OplaxFunctor.mapComp_id_right_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_hom, CategoryTheory.OplaxFunctor.mapComp_assoc_right, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_inv, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Paths.lift_cons, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.id_app, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app, CategoryTheory.ReflPrefunctor.comp_map, CategoryTheory.Pseudofunctor.toLax_mapId, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv, CategoryTheory.Oplax.OplaxTrans.isoMk_hom_as_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom, CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_inv, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, CategoryTheory.OplaxFunctor.map₂_rightUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, CategoryTheory.Pseudofunctor.map₂_left_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, costar_comp, CategoryTheory.Bicategory.Prod.snd_mapId_hom, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_hom, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_assoc, CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.FreeBicategory.normalize_naturality, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id, mapPath_comp, pathStar_apply, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_obj, CategoryTheory.OplaxFunctor.mapComp_id_right, CategoryTheory.Pseudofunctor.toDescentData_obj, CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_hom, costar_conj_star, CategoryTheory.Pseudofunctor.mapComp_id_right_inv, costar_fst, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc, CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_right, CategoryTheory.Bicategory.Prod.sectR_obj, IsCovering.costar_bijective, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, costar_apply, CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.Quiv.inv_obj_hom_obj_of_iso, CategoryTheory.LaxFunctor.map₂_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, CategoryTheory.Bicategory.Prod.snd_mapId_inv, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app, CategoryTheory.Lax.StrongTrans.naturality_naturality, CategoryTheory.Oplax.OplaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv, CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app, symmetrifyStar, CategoryTheory.Pseudofunctor.map₂_right_unitor, CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, Quiver.SingleObj.toPrefunctor_apply_obj, CategoryTheory.PrelaxFunctorStruct.comp_map₂, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, RingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.PrelaxFunctor.map₂_comp, CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.PrelaxFunctor.mapFunctor_obj, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, CategoryTheory.ReflQuiv.id_obj, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app, CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.StrictPseudofunctor.comp_mapComp_inv, star_apply, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_base, CategoryTheory.Lax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, CategoryTheory.Bicategory.InducedBicategory.forget_obj, congr_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.ReflPrefunctor.comp_obj, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.map₂_associator, CategoryTheory.Bicategory.Prod.swap_obj, CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, Quiver.Push.of_reverse, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_assoc, CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp', CategoryTheory.Lax.StrongTrans.id_naturality_hom, CategoryTheory.Lax.OplaxTrans.naturality_id, CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom, CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map, CategoryTheory.PrelaxFunctor.map₂_comp_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app, CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left, CategoryTheory.WithTerminal.pseudofunctor_mapId, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_app, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.PrelaxFunctor.map₂_isIso, CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_obj, symmetrifyCostar, CategoryTheory.LaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, CategoryTheory.StrictPseudofunctor.comp_map₂, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc, CategoryTheory.PrelaxFunctor.map₂_inv_hom_assoc, CategoryTheory.Oplax.StrongTrans.isoMk_inv_as_app, CategoryTheory.Bicategory.Prod.fst_mapComp_inv, CategoryTheory.Oplax.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom, mapPath_cons, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc, congr_obj, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, CategoryTheory.StrictlyUnitaryPseudofunctor.map_id, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_left_app, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const, costar_snd, CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff, CategoryTheory.Bicategory.Prod.snd_mapComp_hom, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.PrelaxFunctor.map₂_id, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app, CategoryTheory.Oplax.OplaxTrans.isoMk_inv_as_app, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map, CategoryTheory.StrictPseudofunctor.mk''_mapComp, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality, CategoryTheory.Oplax.StrongTrans.id_naturality_hom, CategoryTheory.LaxFunctor.mapComp_assoc_left, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, IsCovering.pathStar_bijective, CategoryTheory.LaxFunctor.mapComp_assoc_right, CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_map, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapComp, CategoryTheory.Oplax.StrongTrans.naturality_naturality, CategoryTheory.PrelaxFunctor.map₂Iso_hom, CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app, CategoryTheory.PrelaxFunctor.map₂Iso_inv, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.DescentData.id_hom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.OplaxFunctor.mapComp_id_left_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapId, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Bicategory.Prod.swap_mapComp_hom, CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc, IsCovering.map_injective, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Cat.freeReflMap_map, CategoryTheory.FreeBicategory.of_obj, CategoryTheory.Pseudofunctor.mapId'_hom_naturality, CategoryTheory.Pseudofunctor.DescentData.hom_self, CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, CategoryTheory.FreeBicategory.lift_mapComp, SSet.OneTruncation₂.map_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, symmetrify_map, CategoryTheory.Oplax.StrongTrans.toOplax_naturality, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, star_comp, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Pseudofunctor.comp_mapComp, star_snd, CategoryTheory.Bicategory.Prod.swap_mapComp_inv, CategoryTheory.PrelaxFunctor.map₂Iso_eqToIso, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp, CategoryTheory.Pseudofunctor.toOplax_mapId', CategoryTheory.Bicategory.Prod.snd_mapComp_inv, CategoryTheory.StrictPseudofunctor.mk''_obj, CategoryTheory.Pseudofunctor.map₂_whisker_right_app, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality, CategoryTheory.Quiv.hom_obj_inv_obj_of_iso, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.FreeBicategory.preinclusion_obj, CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.LaxFunctor.comp_mapComp, CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso_assoc, CategoryTheory.PrelaxFunctor.map₂_inv_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, CategoryTheory.Bicategory.Prod.swap_mapId_hom, CategoryTheory.zigzag_prefunctor_obj_of_zigzag, CategoryTheory.LaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.toLax_mapComp', CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc, CategoryTheory.StrictPseudofunctor.comp_obj, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, CategoryTheory.Paths.lift_nil, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Cat.FreeRefl.lift_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq, CategoryTheory.LaxFunctor.mapComp_naturality_left, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc, CategoryTheory.Paths.of_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc, CategoryTheory.Bicategory.InducedBicategory.forget_mapId_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.Bicategory.Prod.fst_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_inv, mapPath_comp_apply, CategoryTheory.Pseudofunctor.comp_mapId, CategoryTheory.Bicategory.Prod.swap_mapId_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, symmetrify_obj, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc, bijective_costar_iff_bijective_star, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_inv, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Lax.OplaxTrans.id_app, CategoryTheory.ReflPrefunctor.mk_obj, CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app, CategoryTheory.Functor.toPseudoFunctor_obj, CategoryTheory.LaxFunctor.map₂_leftUnitor_app, CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map₂, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app, CategoryTheory.Pseudofunctor.whiskerRightIso_mapId, CategoryTheory.Pseudofunctor.Grothendieck.map_map_base, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app, CategoryTheory.Pseudofunctor.toOplax_mapComp', CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom, CategoryTheory.Bicategory.Prod.fst_mapId_inv, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom, CategoryTheory.Oplax.OplaxTrans.Modification.id_app, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_obj, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso, CategoryTheory.OplaxFunctor.mapComp_id_left, CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.LaxFunctor.map₂_rightUnitor, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.FreeBicategory.liftHom_comp, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map₂, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, CategoryTheory.Cat.freeMapCompIso_inv_app, CategoryTheory.Quiv.equivOfIso_apply, CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Prefunctor.mapPath_comp'
«term_⋙q_» 📖	CompOp	—
«term_⥤q_» 📖	CompOp	—
«term𝟭q» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	—
comp_map 📖	mathematical	—	map comp obj	—	—
comp_obj 📖	mathematical	—	obj comp	—	—
congr_hom 📖	mathematical	—	Quiver.homOfEq obj map congr_obj	—	congr_obj
congr_map 📖	mathematical	—	map	—	—
congr_obj 📖	mathematical	—	obj	—	—
ext 📖	—	obj map Quiver.Hom	—	—	—
ext' 📖	—	obj map Quiver.homOfEq	—	—	—
homOfEq_map 📖	mathematical	—	map Quiver.homOfEq obj	—	—
id_comp 📖	mathematical	—	comp id	—	—
id_map 📖	mathematical	—	map id	—	—
id_obj 📖	mathematical	—	obj id	—	—
mk_map 📖	mathematical	—	map	—	—
mk_obj 📖	mathematical	—	obj	—	—

(root)

Definitions

Name	Category	Theorems
Prefunctor 📖	CompData	8 math math: Quiver.SingleObj.toPrefunctor_symm_id, Quiver.SingleObj.toPrefunctor_apply_map, Quiver.SingleObj.toPrefunctor_comp, CategoryTheory.Quiv.adj_homEquiv, Quiver.SingleObj.toPrefunctor_id, Quiver.SingleObj.toPrefunctor_apply_obj, Quiver.SingleObj.toPrefunctor_symm_comp, Quiver.SingleObj.toPrefunctor_symm_apply

---

← Back to Index