Cat

📁 Source: Mathlib/CategoryTheory/Category/Cat.lean

Statistics

Metric	Count
Definitions equivFunctor, instCategory, instQuiver, isoMk, toFunctor, toNatIso, Hom₂, toNatTrans, bicategory, category, equivOfIso, instCategoryObjObjects, instCoeSortType, instInhabited, instQuiver, isoOfEquiv, objects, of, str, equivCatHom, toCatHom, toCatHom₂, typeToCat	23
Theorems comp_map, comp_obj, comp_toFunctor, equivFunctor_apply, equivFunctor_symm_apply, ext, ext_iff, hom_inv_id_toNatTrans, hom_inv_id_toNatTrans_app, hom_inv_id_toNatTrans_app_assoc, hom_inv_id_toNatTrans_assoc, id_map, id_obj, id_toFunctor, instIsIsoFunctorαCategoryToNatTransHomHom, instIsIsoFunctorαCategoryToNatTransInvHom, inv_hom_id_toNatTrans, inv_hom_id_toNatTrans_app, inv_hom_id_toNatTrans_app_assoc, inv_hom_id_toNatTrans_assoc, isoMk_hom, isoMk_inv, isoMk_toNatIso, toNatIso_associator, toNatIso_hom, toNatIso_inv, toNatIso_isoMk, toNatIso_leftUnitor, toNatIso_rightUnitor, toNatTrans_comp, toNatTrans_id, comp_app, comp_app_assoc, eqToHom_toNatTrans, ext, ext_iff, id_app, associator_hom_app, associator_hom_toNatTrans, associator_inv_app, associator_inv_toNatTrans, strict, coe_of, comp_eq_comp, eqToHom_app, ext, ext_iff, id_eq_id, isoOfEquiv_hom, isoOfEquiv_inv, leftUnitor_hom_app, leftUnitor_hom_toNatTrans, leftUnitor_inv_app, leftUnitor_inv_toNatTrans, of_α, rightUnitor_hom_app, rightUnitor_hom_toNatTrans, rightUnitor_inv_app, rightUnitor_inv_toNatTrans, whiskerLeft_app, whiskerLeft_toNatTrans, whiskerRight_app, whiskerRight_toNatTrans, equivCatHom_apply, equivCatHom_symm_apply, toCatHom_toFunctor, toCatHom₂_comp, toCatHom₂_id, toCatHom₂_toNatTrans, instFaithfulCatTypeToCat, instFullCatTypeToCat, typeToCat_map, typeToCat_obj	73
Total	96

CategoryTheory

Definitions

Name	Category	Theorems
typeToCat 📖	CompOp	22 math math: Grothendieck.grothendieckTypeToCat_inverse_map_base, Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe, instFullCatTypeToCat, Grothendieck.grothendieckTypeToCatFunctor_obj_snd, Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base, Grothendieck.grothendieckTypeToCat_functor_obj_fst, Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base, Grothendieck.grothendieckTypeToCat_inverse_obj_base, Grothendieck.grothendieckTypeToCatFunctor_map_coe, Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe, Grothendieck.grothendieckTypeToCatFunctor_obj_fst, Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as, instFaithfulCatTypeToCat, typeToCat_obj, typeToCat_map, Grothendieck.grothendieckTypeToCatInverse_obj_base, Grothendieck.grothendieckTypeToCatInverse_map_base, Grothendieck.grothendieckTypeToCat_functor_map_coe, Grothendieck.grothendieckTypeToCat_functor_obj_snd, Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulCatTypeToCat 📖	mathematical	—	Functor.Faithful types Cat Cat.category typeToCat	—	Functor.congr_obj
instFullCatTypeToCat 📖	mathematical	—	Functor.Full types Cat Cat.category typeToCat	—	Cat.ext Functor.ext Discrete.ext ULift.ext Category.comp_id Category.id_comp
typeToCat_map 📖	mathematical	—	Functor.map types Cat Cat.category typeToCat Functor.toCatHom Discrete discreteCategory Discrete.functor	—	—
typeToCat_obj 📖	mathematical	—	Functor.obj types Cat Cat.category typeToCat Cat.of Discrete discreteCategory	—	—

CategoryTheory.Cat

Definitions

Name	Category	Theorems
Hom₂ 📖	CompData	—
bicategory 📖	CompOp	326 math math: CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, whiskerRight_toNatTrans, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, Hom.id_map, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, Hom.toNatIso_associator, associator_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_eq, CategoryTheory.Adjunction.ofCat_counit, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, 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.Pseudofunctor.DescentData.isoMk_inv_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.Grothendieck.map_id_eq, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l, CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.DescentData.comp_hom, leftUnitor_hom_app, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app, CategoryTheory.Adjunction.toCat_comp_toCat, CategoryTheory.Pseudofunctor.Grothendieck.ext_iff, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, CategoryTheory.Pseudofunctor.map₂_associator_app, rightUnitor_hom_toNatTrans, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.iso_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, associator_inv_app, Hom.comp_toFunctor, rightUnitor_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, CategoryTheory.Pseudofunctor.Grothendieck.map_id_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.OplaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.LaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app, CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app, CategoryTheory.Adjunction.toCat_counit_toNatTrans, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, CategoryTheory.Bicategory.Adjunction.ofCat_id, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber, CategoryTheory.Bicategory.Adjunction.ofCat_comp, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, 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.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, Hom.comp_map, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, 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.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_fiber, CategoryTheory.Pseudofunctor.isStackFor_iff, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.WithInitial.pseudofunctor_mapId, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, RingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, comp_eq_comp, leftUnitor_hom_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj, CategoryTheory.WithInitial.pseudofunctor_toPrelaxFunctor, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, CategoryTheory.Bicategory.toNatTrans_mateEquiv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, associator_inv_toNatTrans, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.map₂_left_unitor_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.Pseudofunctor.toDescentData_obj, Hom.toNatIso_leftUnitor, CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, Hom.toNatIso_rightUnitor, Hom.id_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.WithTerminal.pseudofunctor_toPrelaxFunctor, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, rightUnitor_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc, rightUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.Adjunction.toCat_unit_toNatTrans, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, Hom.comp_obj, RingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.Pseudofunctor.Grothendieck.map_comp_eq, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_base, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.WithTerminal.pseudofunctor_mapId, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.LaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl, CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_left_app, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_eq, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl, CategoryTheory.Adjunction.ofCat_unit, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, id_eq_id, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.Pseudofunctor.DescentData.id_hom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, bicategory.strict, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, 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.Pseudofunctor.ObjectProperty.map_obj_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, whiskerLeft_toNatTrans, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, CategoryTheory.Pseudofunctor.map₂_whisker_right_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_map, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, whiskerRight_app, CategoryTheory.LaxFunctor.map₂_associator_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, associator_hom_toNatTrans, Hom.id_toFunctor, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, leftUnitor_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_app, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr, whiskerLeft_app, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_map_base, CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, 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
category 📖	CompOp	244 math math: SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, asSmallFunctor_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber, CategoryTheory.Grpd.forgetToCat_full, CategoryTheory.ReflQuiv.adj_homEquiv, freeRefl_map, CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂, CategoryTheory.curryingIso_hom_toFunctor_obj_map, CategoryTheory.nerve.functorOfNerveMap_map, CategoryTheory.Grothendieck.map_comp_eq, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, CategoryTheory.Grothendieck.pre_comp_map_assoc, CategoryTheory.Grpd.free_obj, CategoryTheory.Grothendieck.ιNatTrans_app_fiber, CategoryTheory.nerveFunctor.faithful, SSet.hoFunctor.preservesTerminal', CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base, CategoryTheory.CostructuredArrow.functor_obj, CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe, CategoryTheory.Grpd.free_map, CategoryTheory.instFullCatTypeToCat, CategoryTheory.Monoidal.whiskerRight_fst, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, CategoryTheory.Grothendieck.isoMk_inv_fiber, CategoryTheory.ReflQuiv.adj_unit_app, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, CategoryTheory.Under.mapFunctor_obj, exp_obj, opEquivalence_counitIso, MonCat.toCat_faithful, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app, CategoryTheory.Grothendieck.id_fiber, ihom_obj, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, CategoryTheory.flippingIso_inv_toFunctor_obj_map_app, CategoryTheory.StructuredArrow.functor_map, instHasTerminal, HasLimits.limitCone_π_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right, free_map, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base, HasLimits.limitCone_pt, HasLimits.homDiagram_map, CategoryTheory.Grothendieck.ιNatTrans_app_base, opFunctor_obj, CategoryTheory.Grothendieck.comp_fiber, CategoryTheory.Grothendieck.map_map, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base, CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber, instFaithfulPreordCatPreordToCat, CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂, CategoryTheory.Monoidal.whiskerRight, SSet.hoFunctor.unitHomEquiv_eq, HasLimits.limitConeX_α, CategoryTheory.ReflQuiv.forget_map, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst, CategoryTheory.Monoidal.tensorHom, CategoryTheory.ReflQuiv.adj.unit.map_app_eq, CategoryTheory.hoFunctor.preservesFiniteProducts, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, CategoryTheory.curryingIso_inv_toFunctor_obj_map_app, CategoryTheory.Grothendieck.fiber_eqToHom, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, CategoryTheory.Monoidal.rightUnitor_hom, CategoryTheory.Grothendieck.eqToHom_eq, CategoryTheory.curryingIso_hom_toFunctor_obj_obj, opEquivalence_unitIso, CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor, CategoryTheory.Quiv.forget_map, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left, SimplexCategory.toCat.obj_eq_Fin, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber, exp_map, CategoryTheory.CatEnrichedOrdinary.Hom.id_eq, CategoryTheory.ReflQuiv.forget_obj, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, isoOfEquiv_inv, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe, CategoryTheory.Quiv.adj_homEquiv, isoOfEquiv_hom, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber, SSet.hoFunctor.preservesTerminal, HasLimits.limit_π_homDiagram_eqToHom, CategoryTheory.Grothendieck.pre_map_fiber, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app, opFunctor_map, CategoryTheory.flippingIso_inv_toFunctor_map_app_app, CategoryTheory.Grothendieck.map_id_eq, opFunctorInvolutive_hom_app_toFunctor_map, opFunctorInvolutive_hom_app_toFunctor_obj, HasLimits.limitConeX_str, instHasLimits, CategoryTheory.CostructuredArrow.functor_map, CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe, CategoryTheory.Monoidal.associator_hom, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor, opEquivalence_inverse, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, CategoryTheory.Under.mapFunctor_map, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso, CategoryTheory.Grpd.forgetToCat_faithful, CategoryTheory.ReflQuiv.forget_forgetToQuiv, CategoryTheory.nerveFunctor_map, CategoryTheory.Grothendieck.toTransport_fiber, CategoryTheory.Codiscrete.adj_counit_app, HasLimits.id_def, CategoryTheory.Monoidal.whiskerLeft_snd, CategoryTheory.CatEnrichedOrdinary.Hom.base_comp, free_obj, CategoryTheory.Grothendieck.pre_obj_base, opEquivalence_functor, opFunctorInvolutive_inv_app_toFunctor_map, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map, CategoryTheory.Functor.elementsFunctor_map, CategoryTheory.CostructuredArrow.grothendieckProj_map, SSet.Truncated.hoFunctor₂_naturality, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst, CategoryTheory.Grpd.freeForgetAdjunction_counit_app, CategoryTheory.ReflQuiv.adj_counit_app, CategoryTheory.hoFunctor.preservesBinaryProducts, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse, CategoryTheory.Grothendieck.pre_comp_map, instFullPreordCatPreordToCat, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse, CategoryTheory.Grothendieck.map_obj_fiber, CategoryTheory.ReflQuiv.forget.Faithful, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base, ihom_map, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex, CategoryTheory.CostructuredArrow.preFunctor_app, CategoryTheory.Monoidal.tensorUnit, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq, CategoryTheory.Grothendieck.ιCompMap_inv_app_base, CategoryTheory.nerve_map, CategoryTheory.CatEnriched.comp_eq, CategoryTheory.Grothendieck.pre_comp, MonCat.toCat_full, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.nerveFunctor.full, CategoryTheory.Grothendieck.transportIso_inv_fiber, CategoryTheory.CatEnrichedOrdinary.homEquiv_comp, CategoryTheory.Grothendieck.map_obj, opFunctorInvolutive_inv_app_toFunctor_obj, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base, CategoryTheory.flippingIso_hom_toFunctor_obj_map_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso, CategoryTheory.CostructuredArrow.grothendieckProj_obj, freeRefl_obj, preordToCat_obj, CategoryTheory.Functor.elementsFunctor_obj, preordToCat_map, CategoryTheory.Codiscrete.adj_unit_app, CategoryTheory.curryingIso_inv_toFunctor_map_app_app, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, CategoryTheory.Grothendieck.final_pre, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.StructuredArrow.functor_obj, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_unitIso, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as, CategoryTheory.CatEnriched.id_eq, SimplexCategory.toCat_obj, HasLimits.comp_def, CategoryTheory.Over.mapFunctor_obj, CategoryTheory.Monoidal.whiskerRight_snd, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app, CategoryTheory.instFaithfulCatTypeToCat, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_map, CategoryTheory.hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.hoFunctor.preservesBinaryProduct, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, CategoryTheory.Grothendieck.transport_fiber, HasLimits.limitConeLift_toFunctor, CategoryTheory.nerveFunctor_obj, CategoryTheory.Grothendieck.map_map_fiber, CategoryTheory.typeToCat_obj, asSmallFunctor_map, CategoryTheory.Monoidal.associator_inv, CategoryTheory.Grothendieck.map_map_base, CategoryTheory.Monoidal.rightUnitor_inv, CategoryTheory.Monoidal.whiskerLeft, CategoryTheory.Grothendieck.ι_obj, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_obj, CategoryTheory.typeToCat_map, CategoryTheory.flippingIso_hom_toFunctor_map_app_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right, CategoryTheory.Grothendieck.ιCompMap_hom_app_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, CategoryTheory.Monoidal.tensorObj, instPreservesLimitsObjects, CategoryTheory.Grothendieck.pre_obj_fiber, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map, CategoryTheory.nerve.functorOfNerveMap_obj, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app, CategoryTheory.Monoidal.whiskerLeft_fst, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, CategoryTheory.Grpd.freeForgetAdjunction_unit_app, CategoryTheory.Grothendieck.pre_id, SimplexCategory.toCat_map, HasLimits.homDiagram_obj, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base, CategoryTheory.Grothendieck.congr, CategoryTheory.Over.mapFunctor_map, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe, CategoryTheory.Grothendieck.isoMk_hom_fiber, CategoryTheory.Monoidal.leftUnitor_inv, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd, CategoryTheory.hoFunctor.isIso_prodComparison, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_counitIso, CategoryTheory.curryingIso_hom_toFunctor_map_app, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as, CategoryTheory.nerveAdjunction.isIso_counit, CategoryTheory.CatEnrichedOrdinary.homEquiv_id, instHasColimits, CategoryTheory.Monoidal.leftUnitor_hom, CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom, CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂, CategoryTheory.Quiv.forget_obj, CategoryTheory.Grothendieck.transportIso_hom_fiber, CategoryTheory.Grothendieck.pre_map_base, CategoryTheory.Grothendieck.ι_map, CategoryTheory.Grothendieck.faithful_ι, CategoryTheory.CatEnrichedOrdinary.Hom.base_id
equivOfIso 📖	CompOp	—
instCategoryObjObjects 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instInhabited 📖	CompOp	—
instQuiver 📖	CompOp	47 math math: CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, Hom₂.comp_app, CategoryTheory.ReflQuiv.adj_homEquiv, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, Hom.inv_hom_id_toNatTrans_assoc, Hom₂.eqToHom_toNatTrans, Hom₂.id_app, Hom.isoMk_hom, Hom.toNatIso_hom, CategoryTheory.Functor.equivCatHom_symm_apply, Hom₂.comp_app_assoc, Hom.inv_hom_id_toNatTrans, Hom.isoMk_inv, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Functor.equivCatHom_apply, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.NatTrans.toCatHom₂_id, Hom.hom_inv_id_toNatTrans, CategoryTheory.Quiv.adj_homEquiv, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, Hom.hom_inv_id_toNatTrans_assoc, Hom.inv_hom_id_toNatTrans_app_assoc, Hom.instIsIsoFunctorαCategoryToNatTransInvHom, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, Hom.toNatTrans_id, CategoryTheory.NatTrans.toCatHom₂_comp, Hom.hom_inv_id_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, Hom.toNatTrans_comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, Hom.inv_hom_id_toNatTrans_app, Hom.hom_inv_id_toNatTrans_app_assoc, Hom.equivFunctor_apply, Hom.toNatIso_inv, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, Hom.instIsIsoFunctorαCategoryToNatTransHomHom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, Hom.equivFunctor_symm_apply, eqToHom_app
isoOfEquiv 📖	CompOp	2 math math: isoOfEquiv_inv, isoOfEquiv_hom
objects 📖	CompOp	12 math math: HasLimits.limitCone_π_app, HasLimits.homDiagram_map, HasLimits.limitConeX_α, HasLimits.limit_π_homDiagram_eqToHom, HasLimits.limitConeX_str, CategoryTheory.Codiscrete.adj_counit_app, HasLimits.id_def, CategoryTheory.Codiscrete.adj_unit_app, HasLimits.comp_def, HasLimits.limitConeLift_toFunctor, instPreservesLimitsObjects, HasLimits.homDiagram_obj
of 📖	CompOp	115 math math: CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, asSmallFunctor_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.ReflQuiv.adj_homEquiv, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.curryingIso_hom_toFunctor_obj_map, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.nerve.functorOfNerveMap_map, of_α, CategoryTheory.CostructuredArrow.functor_obj, Hom.isoMk_hom, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, CategoryTheory.Functor.equivCatHom_symm_apply, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.Adjunction.toCat_comp_toCat, Hom.isoMk_inv, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, Hom.toNatIso_isoMk, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, CategoryTheory.Under.mapFunctor_obj, exp_obj, ihom_obj, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.flippingIso_inv_toFunctor_obj_map_app, CategoryTheory.Functor.equivCatHom_apply, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, opFunctor_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans, CategoryTheory.Adjunction.toCat_counit_toNatTrans, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.NatTrans.toCatHom₂_id, CategoryTheory.curryingIso_inv_toFunctor_obj_map_app, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, CategoryTheory.curryingIso_hom_toFunctor_obj_obj, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, CategoryTheory.Quiv.adj_homEquiv, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl, CategoryTheory.flippingIso_inv_toFunctor_map_app_app, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, free_obj, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map, CategoryTheory.CostructuredArrow.grothendieckProj_map, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, coe_of, CategoryTheory.ReflQuiv.adj_counit_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, ihom_map, AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.NatTrans.toCatHom₂_toNatTrans, CategoryTheory.Adjunction.ofCat_toCat, CategoryTheory.Adjunction.toCat_unit_toNatTrans, RingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply, CategoryTheory.NatTrans.toCatHom₂_comp, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.flippingIso_hom_toFunctor_obj_map_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, freeRefl_obj, preordToCat_obj, CategoryTheory.Functor.elementsFunctor_obj, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.curryingIso_inv_toFunctor_map_app_app, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, CategoryTheory.StructuredArrow.functor_obj, SimplexCategory.toCat_obj, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Over.mapFunctor_obj, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_map, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, CategoryTheory.typeToCat_obj, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_obj, CategoryTheory.flippingIso_hom_toFunctor_map_app_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CategoryTheory.Monoidal.tensorObj, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map, CategoryTheory.nerve.functorOfNerveMap_obj, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, CategoryTheory.Grpd.freeForgetAdjunction_unit_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, Hom.equivFunctor_apply, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.curryingIso_hom_toFunctor_map_app, CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.Functor.toCatHom_toFunctor, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map
str 📖	CompOp	434 math math: CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, Hom₂.comp_app, whiskerRight_toNatTrans, asSmallFunctor_obj, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber, CategoryTheory.ReflQuiv.adj_homEquiv, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, Hom.id_map, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, Hom.toNatIso_associator, associator_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, Hom.inv_hom_id_toNatTrans_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.curryingIso_hom_toFunctor_obj_map, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.nerve.functorOfNerveMap_map, CategoryTheory.Adjunction.ofCat_counit, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Grpd.free_obj, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, Hom₂.eqToHom_toNatTrans, Hom₂.id_app, CategoryTheory.Grothendieck.ιNatTrans_app_fiber, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Grpd.free_map, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc, Hom.toNatIso_hom, 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.Monoidal.whiskerRight_fst, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom, Hom₂.comp_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, Hom.isoMk_toNatIso, CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.DescentData.comp_hom, leftUnitor_hom_app, CategoryTheory.Grothendieck.isoMk_inv_fiber, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app, Hom.inv_hom_id_toNatTrans, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, exp_obj, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, opEquivalence_counitIso, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app, CategoryTheory.Grothendieck.id_fiber, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, CategoryTheory.Pseudofunctor.map₂_associator_app, rightUnitor_hom_toNatTrans, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.flippingIso_inv_toFunctor_obj_map_app, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.iso_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, HasLimits.homDiagram_map, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, associator_inv_app, Hom.comp_toFunctor, CategoryTheory.Grothendieck.ιNatTrans_app_base, rightUnitor_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality, opFunctor_obj, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Grothendieck.comp_fiber, CategoryTheory.Grothendieck.map_map, CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.Monoidal.whiskerRight, CategoryTheory.OplaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.LaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans, SSet.hoFunctor.unitHomEquiv_eq, CategoryTheory.ReflQuiv.forget_map, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app, CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc, CategoryTheory.Monoidal.tensorHom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, CategoryTheory.Bicategory.Adjunction.ofCat_id, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber, CategoryTheory.Bicategory.Adjunction.ofCat_comp, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, CategoryTheory.curryingIso_inv_toFunctor_obj_map_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.Grothendieck.fiber_eqToHom, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, CategoryTheory.Monoidal.rightUnitor_hom, CategoryTheory.Grothendieck.eqToHom_eq, CategoryTheory.curryingIso_hom_toFunctor_obj_obj, opEquivalence_unitIso, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, CategoryTheory.Quiv.forget_map, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber, Hom.hom_inv_id_toNatTrans, exp_map, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app, CategoryTheory.ReflQuiv.forget_obj, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Functor.toReflPrefunctor_toPrefunctor, CategoryTheory.Quiv.adj_homEquiv, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app, opFunctor_map, CategoryTheory.flippingIso_inv_toFunctor_map_app_app, Hom.comp_map, opFunctorInvolutive_hom_app_toFunctor_map, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, opFunctorInvolutive_hom_app_toFunctor_obj, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber, CategoryTheory.Monoidal.associator_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_fiber, CategoryTheory.Pseudofunctor.isStackFor_iff, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber, CategoryTheory.nerveFunctor_map, CategoryTheory.Grothendieck.toTransport_fiber, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.Monoidal.whiskerLeft_snd, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, opFunctorInvolutive_inv_app_toFunctor_map, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map, CategoryTheory.CostructuredArrow.grothendieckProj_map, SSet.Truncated.hoFunctor₂_naturality, coe_of, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.WithInitial.pseudofunctor_mapId, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, CategoryTheory.Grothendieck.map_obj_fiber, comp_eq_comp, leftUnitor_hom_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, CategoryTheory.Adjunction.toCat_ofCat, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, CategoryTheory.Bicategory.toNatTrans_mateEquiv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, Hom.hom_inv_id_toNatTrans_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, associator_inv_toNatTrans, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.map₂_left_unitor_app, Hom.inv_hom_id_toNatTrans_app_assoc, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.Grothendieck.ιCompMap_inv_app_base, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.CatEnriched.comp_eq, Hom.instIsIsoFunctorαCategoryToNatTransInvHom, CategoryTheory.Pseudofunctor.toDescentData_obj, Hom.toNatIso_leftUnitor, CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, Hom.toNatIso_rightUnitor, Hom.id_obj, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, CategoryTheory.Grothendieck.transportIso_inv_fiber, rightUnitor_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Grothendieck.map_obj, Hom.toNatTrans_id, opFunctorInvolutive_inv_app_toFunctor_obj, rightUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, Hom.comp_obj, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_base, CategoryTheory.flippingIso_hom_toFunctor_obj_map_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Codiscrete.adj_unit_app, CategoryTheory.curryingIso_inv_toFunctor_map_app_app, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, CategoryTheory.WithTerminal.pseudofunctor_mapId, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.LaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc, CategoryTheory.CatEnriched.id_eq, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, Hom.hom_inv_id_toNatTrans_app, CategoryTheory.Monoidal.whiskerRight_snd, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl, CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_map, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.Pseudofunctor.map₂_whisker_left_app, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map, CategoryTheory.Grothendieck.transport_fiber, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc, HasLimits.limitConeLift_toFunctor, CategoryTheory.nerveFunctor_obj, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, CategoryTheory.Grothendieck.map_map_fiber, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, asSmallFunctor_map, CategoryTheory.Monoidal.associator_inv, CategoryTheory.Grothendieck.map_map_base, CategoryTheory.Monoidal.rightUnitor_inv, CategoryTheory.Monoidal.whiskerLeft, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl, CategoryTheory.Grothendieck.ι_obj, CategoryTheory.Adjunction.ofCat_unit, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, Hom.toNatTrans_comp, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, id_eq_id, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_obj, CategoryTheory.Pseudofunctor.DescentData.id_hom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom, CategoryTheory.flippingIso_hom_toFunctor_map_app_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.Grothendieck.ιCompMap_hom_app_base, CategoryTheory.Pseudofunctor.mapId'_hom_naturality, CategoryTheory.Pseudofunctor.DescentData.hom_self, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app, Hom.inv_hom_id_toNatTrans_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, CategoryTheory.Monoidal.tensorObj, Hom.hom_inv_id_toNatTrans_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, whiskerLeft_toNatTrans, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, CategoryTheory.Pseudofunctor.map₂_whisker_right_app, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.nerve.functorOfNerveMap_obj, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.Monoidal.whiskerLeft_fst, CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, Hom.equivFunctor_apply, Hom.toNatIso_inv, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, whiskerRight_app, CategoryTheory.LaxFunctor.map₂_associator_app, CategoryTheory.Grothendieck.congr, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, associator_hom_toNatTrans, Hom.instIsIsoFunctorαCategoryToNatTransHomHom, Hom.id_toFunctor, CategoryTheory.Grothendieck.isoMk_hom_fiber, CategoryTheory.Monoidal.leftUnitor_inv, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.curryingIso_hom_toFunctor_map_app, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, leftUnitor_inv_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, CategoryTheory.Monoidal.leftUnitor_hom, CategoryTheory.LaxFunctor.map₂_leftUnitor_app, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, CategoryTheory.Quiv.forget_obj, CategoryTheory.Grothendieck.transportIso_hom_fiber, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, Hom.equivFunctor_symm_apply, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr, whiskerLeft_app, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_map_base, CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc, eqToHom_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.Grothendieck.ι_map, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, CategoryTheory.Grothendieck.faithful_ι, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, 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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
associator_hom_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toFunctor CategoryTheory.Functor.associator	—	—
associator_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
associator_inv_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toFunctor CategoryTheory.Functor.associator	—	—
coe_of 📖	mathematical	—	of CategoryTheory.Bundled.α CategoryTheory.Category str	—	—
comp_eq_comp 📖	mathematical	—	Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category str	—	—
eqToHom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor Hom₂.toNatTrans CategoryTheory.eqToHom Quiver.Hom CategoryTheory.Cat instQuiver CategoryTheory.Category.toCategoryStruct Hom.instCategory CategoryTheory.Functor.obj Hom	—	CategoryTheory.Functor.congr_obj Hom₂.eqToHom_toNatTrans CategoryTheory.eqToHom_app
ext 📖	—	Hom.toFunctor	—	—	—
ext_iff 📖	mathematical	—	Hom.toFunctor	—	ext
id_eq_id 📖	mathematical	—	Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category str	—	—
isoOfEquiv_hom 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor	CategoryTheory.Iso.hom CategoryTheory.Cat category isoOfEquiv CategoryTheory.Functor.toCatHom	—	—
isoOfEquiv_inv 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor	CategoryTheory.Iso.inv CategoryTheory.Cat category isoOfEquiv CategoryTheory.Functor.toCatHom	—	—
leftUnitor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
leftUnitor_hom_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id Hom.toFunctor CategoryTheory.Functor.leftUnitor	—	—
leftUnitor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
leftUnitor_inv_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id Hom.toFunctor CategoryTheory.Functor.leftUnitor	—	—
of_α 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Category of	—	—
rightUnitor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
rightUnitor_hom_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toFunctor CategoryTheory.Functor.id CategoryTheory.Functor.rightUnitor	—	—
rightUnitor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
rightUnitor_inv_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toFunctor CategoryTheory.Functor.id CategoryTheory.Functor.rightUnitor	—	—
whiskerLeft_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.toNatTrans CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Functor.obj	—	—
whiskerLeft_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Functor.whiskerLeft CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor	—	—
whiskerRight_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory Hom₂.toNatTrans CategoryTheory.Bicategory.whiskerRight CategoryTheory.Functor.map CategoryTheory.Functor.obj	—	—
whiskerRight_toNatTrans 📖	mathematical	—	Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct bicategory CategoryTheory.Bicategory.whiskerRight CategoryTheory.Functor.whiskerRight CategoryTheory.Bundled.α CategoryTheory.Category str Hom.toFunctor	—	—

CategoryTheory.Cat.Hom

Definitions

Name	Category	Theorems
equivFunctor 📖	CompOp	4 math math: CategoryTheory.ReflQuiv.adj_homEquiv, CategoryTheory.Quiv.adj_homEquiv, equivFunctor_apply, equivFunctor_symm_apply
instCategory 📖	CompOp	42 math math: CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, inv_hom_id_toNatTrans_assoc, CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans, CategoryTheory.Cat.Hom₂.id_app, isoMk_hom, toNatIso_hom, CategoryTheory.Cat.Hom₂.comp_app_assoc, inv_hom_id_toNatTrans, isoMk_inv, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Grothendieck.map_map, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.NatTrans.toCatHom₂_id, hom_inv_id_toNatTrans, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, hom_inv_id_toNatTrans_assoc, inv_hom_id_toNatTrans_app_assoc, instIsIsoFunctorαCategoryToNatTransInvHom, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, toNatTrans_id, CategoryTheory.NatTrans.toCatHom₂_comp, hom_inv_id_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, toNatTrans_comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, inv_hom_id_toNatTrans_app, hom_inv_id_toNatTrans_app_assoc, toNatIso_inv, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, instIsIsoFunctorαCategoryToNatTransHomHom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.Cat.eqToHom_app
instQuiver 📖	CompOp	—
isoMk 📖	CompOp	16 math math: isoMk_hom, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, isoMk_toNatIso, isoMk_inv, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, toNatIso_isoMk, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CategoryTheory.WithInitial.pseudofunctor_mapId, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, CategoryTheory.WithTerminal.pseudofunctor_mapId, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, CategoryTheory.WithInitial.pseudofunctor_mapComp
toFunctor 📖	CompOp	339 math math: CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Cat.whiskerRight_toNatTrans, CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, id_map, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, toNatIso_associator, CategoryTheory.Cat.associator_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, inv_hom_id_toNatTrans_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.curryingIso_hom_toFunctor_obj_map, CategoryTheory.Adjunction.ofCat_counit, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans, CategoryTheory.Cat.Hom₂.id_app, CategoryTheory.Grothendieck.ιNatTrans_app_fiber, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Grpd.free_map, CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc, toNatIso_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Monoidal.whiskerRight_fst, CategoryTheory.Functor.equivCatHom_symm_apply, CategoryTheory.Cat.Hom₂.comp_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, isoMk_toNatIso, CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Cat.leftUnitor_hom_app, CategoryTheory.Grothendieck.isoMk_inv_fiber, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app, inv_hom_id_toNatTrans, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app, CategoryTheory.Grothendieck.id_fiber, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, CategoryTheory.Pseudofunctor.map₂_associator_app, CategoryTheory.Cat.rightUnitor_hom_toNatTrans, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.flippingIso_inv_toFunctor_obj_map_app, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.iso_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Cat.HasLimits.homDiagram_map, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Cat.associator_inv_app, comp_toFunctor, CategoryTheory.Grothendieck.ιNatTrans_app_base, CategoryTheory.Cat.rightUnitor_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Grothendieck.comp_fiber, CategoryTheory.Grothendieck.map_map, CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.Monoidal.whiskerRight, CategoryTheory.OplaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.LaxFunctor.map₂_associator_app_assoc, SSet.hoFunctor.unitHomEquiv_eq, CategoryTheory.ReflQuiv.forget_map, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app, CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc, CategoryTheory.Monoidal.tensorHom, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber, CategoryTheory.Bicategory.Adjunction.ofCat_comp, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.curryingIso_inv_toFunctor_obj_map_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.Grothendieck.fiber_eqToHom, SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality, CategoryTheory.Grothendieck.eqToHom_eq, CategoryTheory.curryingIso_hom_toFunctor_obj_obj, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, CategoryTheory.Quiv.forget_map, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, hom_inv_id_toNatTrans, CategoryTheory.Cat.exp_map, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.Cat.opFunctor_map, CategoryTheory.flippingIso_inv_toFunctor_map_app_app, comp_map, CategoryTheory.Cat.opFunctorInvolutive_hom_app_toFunctor_map, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, CategoryTheory.Cat.opFunctorInvolutive_hom_app_toFunctor_obj, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber, CategoryTheory.nerveFunctor_map, CategoryTheory.Grothendieck.toTransport_fiber, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.Monoidal.whiskerLeft_snd, CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_map, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map, SSet.Truncated.hoFunctor₂_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.WithInitial.pseudofunctor_mapId, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, CategoryTheory.Grothendieck.map_obj_fiber, CategoryTheory.Cat.comp_eq_comp, CategoryTheory.Cat.leftUnitor_hom_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, CategoryTheory.Adjunction.toCat_ofCat, CategoryTheory.Bicategory.toNatTrans_mateEquiv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, hom_inv_id_toNatTrans_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.Cat.associator_inv_toNatTrans, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Cat.leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.map₂_left_unitor_app, inv_hom_id_toNatTrans_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.Grothendieck.ιCompMap_inv_app_base, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.nerve_map, CategoryTheory.CatEnriched.comp_eq, instIsIsoFunctorαCategoryToNatTransInvHom, toNatIso_leftUnitor, CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, toNatIso_rightUnitor, id_obj, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, CategoryTheory.Grothendieck.transportIso_inv_fiber, CategoryTheory.Cat.rightUnitor_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Grothendieck.map_obj, toNatTrans_id, CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_obj, CategoryTheory.Cat.rightUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.Cat.ext_iff, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, comp_obj, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.flippingIso_hom_toFunctor_obj_map_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.Pseudofunctor.toDescentData_map_hom, ext_iff, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.curryingIso_inv_toFunctor_map_app_app, CategoryTheory.ReflQuiv.adj.counit.comp_app_eq, CategoryTheory.WithTerminal.pseudofunctor_mapId, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.LaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc, CategoryTheory.CatEnriched.id_eq, CategoryTheory.WithTerminal.pseudofunctor_mapComp, hom_inv_id_toNatTrans_app, CategoryTheory.Monoidal.whiskerRight_snd, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.flippingIso_inv_toFunctor_obj_obj_map, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality, CategoryTheory.Pseudofunctor.map₂_whisker_left_app, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Grothendieck.transport_fiber, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, CategoryTheory.Grothendieck.map_map_fiber, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, CategoryTheory.Cat.asSmallFunctor_map, CategoryTheory.Grothendieck.map_map_base, CategoryTheory.Monoidal.whiskerLeft, CategoryTheory.Adjunction.ofCat_unit, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, toNatTrans_comp, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, CategoryTheory.Cat.id_eq_id, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.flippingIso_hom_toFunctor_obj_obj_obj, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.flippingIso_hom_toFunctor_map_app_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.Grothendieck.ιCompMap_hom_app_base, CategoryTheory.Pseudofunctor.mapId'_hom_naturality, CategoryTheory.Pseudofunctor.DescentData.hom_self, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app, inv_hom_id_toNatTrans_app, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, hom_inv_id_toNatTrans_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, CategoryTheory.Cat.whiskerLeft_toNatTrans, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv, CategoryTheory.Pseudofunctor.map₂_whisker_right_app, CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.Monoidal.whiskerLeft_fst, CategoryTheory.Grpd.freeForgetAdjunction_unit_app, CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, equivFunctor_apply, toNatIso_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, CategoryTheory.Cat.whiskerRight_app, CategoryTheory.LaxFunctor.map₂_associator_app, CategoryTheory.Grothendieck.congr, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.Cat.associator_hom_toNatTrans, instIsIsoFunctorαCategoryToNatTransHomHom, id_toFunctor, CategoryTheory.Grothendieck.isoMk_hom_fiber, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.curryingIso_hom_toFunctor_map_app, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Cat.leftUnitor_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_app, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, CategoryTheory.Grothendieck.transportIso_hom_fiber, CategoryTheory.Pseudofunctor.DescentData.hom_comp, CategoryTheory.Cat.whiskerLeft_app, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_map_base, CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Cat.eqToHom_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, CategoryTheory.Functor.toCatHom_toFunctor, CategoryTheory.Grothendieck.ι_map, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, 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
toNatIso 📖	CompOp	7 math math: toNatIso_associator, toNatIso_hom, isoMk_toNatIso, toNatIso_isoMk, toNatIso_leftUnitor, toNatIso_rightUnitor, toNatIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.obj	—	—
comp_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory	—	—
comp_toFunctor 📖	mathematical	—	toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str	—	—
equivFunctor_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str EquivLike.toFunLike Equiv.instEquivLike equivFunctor toFunctor CategoryTheory.Cat.of CategoryTheory.Bundled.str	—	—
equivFunctor_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFunctor CategoryTheory.Functor.toCatHom CategoryTheory.Bundled.str	—	—
ext 📖	—	toFunctor	—	—	—
ext_iff 📖	mathematical	—	toFunctor	—	ext
hom_inv_id_toNatTrans 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
hom_inv_id_toNatTrans_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id_app
hom_inv_id_toNatTrans_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_toNatTrans_app
hom_inv_id_toNatTrans_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_toNatTrans
id_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory	—	—
id_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory	—	—
id_toFunctor 📖	mathematical	—	toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Functor.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str	—	—
instIsIsoFunctorαCategoryToNatTransHomHom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory	—	CategoryTheory.Iso.isIso_hom
instIsIsoFunctorαCategoryToNatTransInvHom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory	—	CategoryTheory.Iso.isIso_inv
inv_hom_id_toNatTrans 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
inv_hom_id_toNatTrans_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id_app
inv_hom_id_toNatTrans_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj toFunctor CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_toNatTrans_app
inv_hom_id_toNatTrans_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category toFunctor CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_toNatTrans
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of instCategory CategoryTheory.Functor.toCatHom isoMk CategoryTheory.NatTrans.toCatHom₂ CategoryTheory.Functor CategoryTheory.Functor.category	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of instCategory CategoryTheory.Functor.toCatHom isoMk CategoryTheory.NatTrans.toCatHom₂ CategoryTheory.Functor CategoryTheory.Functor.category	—	—
isoMk_toNatIso 📖	mathematical	—	isoMk CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor toNatIso	—	—
toNatIso_associator 📖	mathematical	—	toNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.Bicategory.associator CategoryTheory.Functor.associator CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor	—	—
toNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category toFunctor toNatIso CategoryTheory.Cat.Hom₂.toNatTrans Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory	—	—
toNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category toFunctor toNatIso CategoryTheory.Cat.Hom₂.toNatTrans Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver instCategory	—	—
toNatIso_isoMk 📖	mathematical	—	toNatIso CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom isoMk	—	—
toNatIso_leftUnitor 📖	mathematical	—	toNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.leftUnitor CategoryTheory.Functor.leftUnitor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str toFunctor	—	—
toNatIso_rightUnitor 📖	mathematical	—	toNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Cat CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.rightUnitor CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category CategoryTheory.Functor.comp toFunctor CategoryTheory.Functor.id CategoryTheory.eqToIso CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Iso.trans_refl CategoryTheory.Iso.refl_trans
toNatTrans_comp 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category toFunctor	—	—
toNatTrans_id 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category toFunctor	—	—

CategoryTheory.Cat.Hom₂

Definitions

Name	Category	Theorems
toNatTrans 📖	CompOp	213 math math: CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, comp_app, CategoryTheory.Cat.whiskerRight_toNatTrans, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app, CategoryTheory.Cat.associator_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.Adjunction.ofCat_counit, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, eqToHom_toNatTrans, id_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc, CategoryTheory.Cat.Hom.toNatIso_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, comp_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Cat.leftUnitor_hom_app, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app, CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.Pseudofunctor.map₂_associator_app, CategoryTheory.Cat.rightUnitor_hom_toNatTrans, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Cat.associator_inv_app, CategoryTheory.Cat.rightUnitor_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Grothendieck.map_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.OplaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.LaxFunctor.map₂_associator_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc, Mathlib.Tactic.CategoryTheory.ToApp.toNatTrans_congr, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app, CategoryTheory.Adjunction.toCat_counit_toNatTrans, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, CategoryTheory.Cat.leftUnitor_hom_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, CategoryTheory.Bicategory.toNatTrans_mateEquiv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.Cat.associator_inv_toNatTrans, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Cat.leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.map₂_left_unitor_app, CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransInvHom, CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, CategoryTheory.Cat.rightUnitor_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Cat.Hom.toNatTrans_id, CategoryTheory.Cat.rightUnitor_inv_toNatTrans, CategoryTheory.NatTrans.toCatHom₂_toNatTrans, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.Adjunction.toCat_unit_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.LaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc, CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.map₂_whisker_left_app, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, CategoryTheory.Adjunction.ofCat_unit, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.Cat.Hom.toNatTrans_comp, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.Pseudofunctor.mapId'_hom_naturality, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app, CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app, CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, CategoryTheory.Cat.whiskerLeft_toNatTrans, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv, CategoryTheory.Pseudofunctor.map₂_whisker_right_app, CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.map₂_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.Cat.Hom.toNatIso_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, CategoryTheory.Cat.whiskerRight_app, CategoryTheory.LaxFunctor.map₂_associator_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, CategoryTheory.Cat.associator_hom_toNatTrans, CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransHomHom, ext_iff, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Cat.leftUnitor_inv_app, CategoryTheory.LaxFunctor.map₂_leftUnitor_app, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, CategoryTheory.Cat.whiskerLeft_app, CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom, CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc, CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc, CategoryTheory.Cat.eqToHom_app, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc, CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor toNatTrans CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj	—	—
comp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app toNatTrans Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_app
eqToHom_toNatTrans 📖	mathematical	—	toNatTrans CategoryTheory.eqToHom Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Functor.category CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.Hom	—	—
ext 📖	—	toNatTrans	—	—	—
ext_iff 📖	mathematical	—	toNatTrans	—	ext
id_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor toNatTrans CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.obj	—	—

CategoryTheory.Cat.bicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strict 📖	mathematical	—	CategoryTheory.Bicategory.Strict CategoryTheory.Cat CategoryTheory.Cat.bicategory	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
equivCatHom 📖	CompOp	2 math math: equivCatHom_symm_apply, equivCatHom_apply
toCatHom 📖	CompOp	68 math math: CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, CategoryTheory.Cat.freeRefl_map, CategoryTheory.Cat.Hom.isoMk_hom, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l, CategoryTheory.Adjunction.toCat_comp_toCat, CategoryTheory.Cat.Hom.isoMk_inv, CategoryTheory.Cat.Hom.toNatIso_isoMk, CategoryTheory.Cat.opEquivalence_counitIso, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.StructuredArrow.functor_map, equivCatHom_apply, CategoryTheory.Cat.HasLimits.limitCone_π_app, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Cat.free_map, CategoryTheory.Monoidal.whiskerRight, CategoryTheory.Monoidal.tensorHom, CategoryTheory.Adjunction.toCat_counit_toNatTrans, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.NatTrans.toCatHom₂_id, CategoryTheory.Monoidal.rightUnitor_hom, CategoryTheory.Cat.opEquivalence_unitIso, CategoryTheory.Cat.exp_map, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, CategoryTheory.Cat.isoOfEquiv_inv, CategoryTheory.Cat.isoOfEquiv_hom, CategoryTheory.Cat.opFunctor_map, CategoryTheory.CostructuredArrow.functor_map, CategoryTheory.Monoidal.associator_hom, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, CategoryTheory.Under.mapFunctor_map, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, elementsFunctor_map, CategoryTheory.ReflQuiv.adj_counit_app, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, RingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.Cat.ihom_map, CategoryTheory.CostructuredArrow.preFunctor_app, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, CategoryTheory.NatTrans.toCatHom₂_toNatTrans, CategoryTheory.Adjunction.ofCat_toCat, CategoryTheory.Adjunction.toCat_unit_toNatTrans, CategoryTheory.NatTrans.toCatHom₂_comp, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, preordToCat_map, CategoryTheory.Codiscrete.adj_unit_app, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, CategoryTheory.Cat.asSmallFunctor_map, CategoryTheory.Monoidal.associator_inv, CategoryTheory.Monoidal.rightUnitor_inv, CategoryTheory.Monoidal.whiskerLeft, CategoryTheory.typeToCat_map, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r, CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap, SimplexCategory.toCat_map, CategoryTheory.Over.mapFunctor_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, CategoryTheory.Monoidal.leftUnitor_inv, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.Monoidal.leftUnitor_hom, CategoryTheory.Cat.Hom.equivFunctor_symm_apply, toCatHom_toFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivCatHom_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of EquivLike.toFunLike Equiv.instEquivLike equivCatHom toCatHom	—	—
equivCatHom_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Functor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivCatHom CategoryTheory.Cat.Hom.toFunctor	—	—
toCatHom_toFunctor 📖	mathematical	—	CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of toCatHom	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
toCatHom₂ 📖	CompOp	15 math math: CategoryTheory.Cat.Hom.isoMk_hom, CategoryTheory.Cat.Hom.isoMk_inv, toCatHom₂_id, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂, toCatHom₂_toNatTrans, toCatHom₂_comp, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCatHom₂_comp 📖	mathematical	—	toCatHom₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.toCatHom	—	—
toCatHom₂_id 📖	mathematical	—	toCatHom₂ CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Quiver.Hom CategoryTheory.Cat CategoryTheory.Cat.instQuiver CategoryTheory.Cat.of CategoryTheory.Cat.Hom.instCategory CategoryTheory.Functor.toCatHom	—	—
toCatHom₂_toNatTrans 📖	mathematical	—	CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom toCatHom₂	—	—

---

← Back to Index