Documentation Verification Report

Bundled

📁 Source: Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean

Statistics

Metric	Count
Definitions `Bundled`, `coeSort`, `map`, `of`, `str`, `α`	6
Theorems `coe_mk`	1
Total	7

CategoryTheory

Definitions

Name	Category	Theorems
`Bundled` 📖	CompData	17 math math: `FirstOrder.Language.IsFraisse.is_essentially_countable`, `FirstOrder.Language.empty.isFraisse_finite`, `FirstOrder.Language.IsFraisse.is_nonempty`, `FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg`, `FirstOrder.Language.dlo_age`, `FirstOrder.Language.age.nonempty`, `FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite`, `FirstOrder.Language.isFraisse_finite_linear_order`, `FirstOrder.Language.Embedding.age_subset_age`, `FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo`, `FirstOrder.Language.exists_countable_is_age_of_iff`, `FirstOrder.Language.age.fg_substructure`, `FirstOrder.Language.IsFraisse.is_equiv_invariant`, `FirstOrder.Language.age.countable_quotient`, `FirstOrder.Language.age.is_equiv_invariant`, `FirstOrder.Language.age_directLimit`, `FirstOrder.Language.Structure.FG.mem_age_of_equiv`

CategoryTheory.Bundled

Definitions

Name	Category	Theorems
`coeSort` 📖	CompOp	—
`map` 📖	CompOp	—
`of` 📖	CompOp	—
`str` 📖	CompOp	16 math math: `CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id`, `CategoryTheory.Cat.opEquivalence_counitIso`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app`, `CategoryTheory.Cat.HasLimits.limitCone_π_app`, `CategoryTheory.Cat.opEquivalence_unitIso`, `CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app`, `CategoryTheory.Cat.HasLimits.limitConeX_str`, `Equiv.bundledInduced_str`, `CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp`, `CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor`, `CategoryTheory.Monoidal.rightUnitor_inv`, `CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp`, `CategoryTheory.Cat.Hom.equivFunctor_apply`, `CategoryTheory.Monoidal.leftUnitor_inv`, `CategoryTheory.Cat.Hom.equivFunctor_symm_apply`
`α` 📖	CompOp	485 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.Quiv.equivOfIso_symm_apply`, `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`, `CategoryTheory.Cat.Hom₂.comp_app`, `CategoryTheory.Cat.whiskerRight_toNatTrans`, `CategoryTheory.Cat.asSmallFunctor_obj`, `CategoryTheory.Quiv.comp_eq_comp`, `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.Cat.freeRefl_map`, `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`, `FundamentalGroupoidFunctor.piIso_hom`, `CategoryTheory.Cat.Hom.id_map`, `CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app`, `CategoryTheory.Cat.Hom.toNatIso_associator`, `CategoryTheory.Cat.associator_hom_app`, `CategoryTheory.Quiv.homEquivOfIso_symm_apply`, `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.curryingIso_hom_toFunctor_obj_map`, `CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj`, `FirstOrder.Language.empty.isFraisse_finite`, `CategoryTheory.nerve.functorOfNerveMap_map`, `ContinuousMap.Homotopy.apply_zero_path`, `CategoryTheory.Adjunction.ofCat_counit`, `CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app`, `CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left`, `CategoryTheory.Grpd.piIsoPi_hom_π`, `CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app`, `CategoryTheory.Grpd.free_obj`, `CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app`, `CategoryTheory.Cat.of_α`, `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`, `Equiv.bundledInduced_α`, `CategoryTheory.Grpd.free_map`, `ContinuousMap.Homotopy.evalAt_eq`, `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`, `CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CategoryTheory.Monoidal.whiskerRight_fst`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber`, `CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom`, `CategoryTheory.Cat.Hom₂.comp_app_assoc`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base`, `CategoryTheory.Grpd.id_to_functor`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber`, `FirstOrder.Language.exists_elementarilyEquivalent_card_eq`, `CategoryTheory.Cat.Hom.isoMk_toNatIso`, `CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor`, `CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc`, `CategoryTheory.Pseudofunctor.DescentData.comp_hom`, `CategoryTheory.ReflQuiv.id_map`, `CategoryTheory.Cat.leftUnitor_hom_app`, `CategoryTheory.Grothendieck.isoMk_inv_fiber`, `ContinuousMap.Homotopy.heq_path_of_eq_image`, `CategoryTheory.OplaxFunctor.map₂_leftUnitor_app`, `CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans`, `CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj`, `CategoryTheory.ReflQuiv.comp_map`, `ContinuousMap.Homotopy.eq_path_of_eq_image`, `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.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber`, `CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `CategoryTheory.Cat.exp_obj`, `CategoryTheory.LaxFunctor.mapComp_assoc_right_app`, `CategoryTheory.Cat.opEquivalence_counitIso`, `FirstOrder.Language.dlo_age`, `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`, `FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite`, `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`, `FundamentalGroupoidFunctor.prodToProdTop_obj`, `CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app`, `CategoryTheory.Pseudofunctor.presheafHom_obj`, `FundamentalGroupoidFunctor.prodIso_hom`, `CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app`, `CategoryTheory.Cat.HasLimits.limitCone_π_app`, `CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app`, `CategoryTheory.Cat.free_map`, `CategoryTheory.Pseudofunctor.DescentData.iso_inv`, `CategoryTheory.ReflQuiv.comp_eq_comp`, `CategoryTheory.OplaxFunctor.mapComp_assoc_left_app`, `CategoryTheory.Cat.HasLimits.homDiagram_map`, `CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app`, `CategoryTheory.Quiv.homEquivOfIso_apply`, `CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq`, `CategoryTheory.Cat.associator_inv_app`, `CategoryTheory.Cat.Hom.comp_toFunctor`, `CategoryTheory.Grothendieck.ιNatTrans_app_base`, `FundamentalGroupoidFunctor.piToPiTop_map`, `CategoryTheory.Cat.rightUnitor_hom_app`, `CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc`, `CategoryTheory.Quiv.inv_map_hom_map_of_iso`, `CategoryTheory.Pseudofunctor.ObjectProperty.ι_naturality`, `CategoryTheory.Cat.opFunctor_obj`, `CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc`, `CategoryTheory.Grothendieck.comp_fiber`, `CategoryTheory.Grothendieck.map_map`, `CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber`, `ContinuousMap.Homotopy.apply_one_path`, `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.Cat.HasLimits.limitConeX_α`, `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.ReflQuiv.adj.unit.map_app_eq`, `CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app`, `CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff`, `CategoryTheory.Prefunctor.to_ofQuivHom`, `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`, `FundamentalGroupoidFunctor.projLeft_map`, `CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app`, `CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app`, `CategoryTheory.curryingIso_inv_toFunctor_obj_map_app`, `CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app`, `FirstOrder.Language.isFraisse_finite_linear_order`, `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`, `CategoryTheory.Cat.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`, `SimplexCategory.toCat.obj_eq_Fin`, `CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber`, `CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans`, `CategoryTheory.Cat.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`, `FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo`, `CategoryTheory.Functor.toReflPrefunctor_toPrefunctor`, `CategoryTheory.Quiv.adj_homEquiv`, `FirstOrder.Language.exists_countable_is_age_of_iff`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber`, `CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id`, `CategoryTheory.OplaxFunctor.mapComp_naturality_left_app`, `CategoryTheory.ReflQuiv.forgetToQuiv_obj`, `CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app`, `CategoryTheory.ReflQuiv.comp_obj`, `CategoryTheory.Cat.opFunctor_map`, `CategoryTheory.flippingIso_inv_toFunctor_map_app_app`, `CategoryTheory.Cat.Hom.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.CoGrothendieck.ext_iff`, `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.Quiv.hom_map_inv_map_of_iso`, `CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff`, `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.Cat.free_obj`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj`, `CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_map`, `CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map`, `SSet.Truncated.hoFunctor₂_naturality`, `FirstOrder.Language.IsFraisse.FG`, `CategoryTheory.Cat.coe_of`, `CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app`, `CategoryTheory.WithInitial.pseudofunctor_mapId`, `FirstOrder.Language.exists_elementaryEmbedding_card_eq`, `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.Pseudofunctor.IsStack.essSurj_of_sieve`, `CategoryTheory.Bicategory.toNatTrans_mateEquiv`, `CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc`, `FundamentalGroupoid.map_eq`, `CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_assoc`, `CategoryTheory.ReflQuiv.of_val`, `CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app`, `FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le`, `CategoryTheory.Cat.associator_inv_toNatTrans`, `CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂`, `CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp`, `CategoryTheory.Grpd.id_eq_id`, `CategoryTheory.Cat.leftUnitor_inv_toNatTrans`, `CategoryTheory.Pseudofunctor.map₂_left_unitor_app`, `CategoryTheory.Cat.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.Grpd.coe_of`, `CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app`, `CategoryTheory.ReflQuiv.forgetToQuiv_map`, `CategoryTheory.CatEnriched.comp_eq`, `CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransInvHom`, `CategoryTheory.Pseudofunctor.toDescentData_obj`, `CategoryTheory.Cat.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`, `CategoryTheory.Cat.Hom.toNatIso_rightUnitor`, `CategoryTheory.Cat.Hom.id_obj`, `CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj`, `CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc`, `CategoryTheory.Quiv.inv_obj_hom_obj_of_iso`, `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`, `CategoryTheory.ReflQuiv.id_eq_id`, `CategoryTheory.Cat.Hom.toNatTrans_id`, `CategoryTheory.Cat.opFunctorInvolutive_inv_app_toFunctor_obj`, `CategoryTheory.Cat.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`, `CategoryTheory.Cat.Hom.comp_obj`, `CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app`, `CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr`, `CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber`, `CategoryTheory.ReflQuiv.id_obj`, `CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc`, `CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `CategoryTheory.Pseudofunctor.mapComp'_naturality_2`, `FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge`, `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`, `FundamentalGroupoidFunctor.piToPiTop_obj_as`, `CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc`, `CategoryTheory.Pseudofunctor.toDescentData_map_hom`, `CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms`, `CategoryTheory.Cat.freeRefl_obj`, `CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc`, `FundamentalGroupoidFunctor.piIso_inv`, `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`, `FundamentalGroupoidFunctor.prodIso_inv`, `CategoryTheory.WithTerminal.pseudofunctor_mapId`, `CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber`, `CategoryTheory.Pseudofunctor.IsStackFor.essSurj`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `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`, `CategoryTheory.CatEnriched.id_eq`, `FundamentalGroupoidFunctor.projRight_map`, `CategoryTheory.WithTerminal.pseudofunctor_mapComp`, `CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj`, `CategoryTheory.Cat.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`, `CategoryTheory.Grpd.comp_eq_comp`, `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`, `CategoryTheory.Cat.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`, `CategoryTheory.Cat.asSmallFunctor_map`, `coe_mk`, `CategoryTheory.Monoidal.associator_inv`, `CategoryTheory.Grothendieck.map_map_base`, `CategoryTheory.Monoidal.rightUnitor_inv`, `CategoryTheory.Monoidal.whiskerLeft`, `CategoryTheory.Grothendieck.ι_obj`, `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.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.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`, `CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app`, `CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId`, `CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj`, `CategoryTheory.Monoidal.tensorObj`, `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.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp`, `CategoryTheory.Pseudofunctor.map₂_whisker_right_app`, `CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map`, `CategoryTheory.Quiv.hom_obj_inv_obj_of_iso`, `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.Quiv.id_eq_id`, `CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj`, `CategoryTheory.Grpd.hom_to_functor`, `CategoryTheory.Cat.Hom.equivFunctor_apply`, `CategoryTheory.Cat.Hom.toNatIso_inv`, `CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc`, `CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `FundamentalGroupoidFunctor.prodToProdTop_map`, `CategoryTheory.Cat.whiskerRight_app`, `CategoryTheory.LaxFunctor.map₂_associator_app`, `CategoryTheory.Grothendieck.congr`, `CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc`, `FundamentalGroupoidFunctor.proj_map`, `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`, `CategoryTheory.Cat.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`, `FirstOrder.Language.Structure.FG.mem_age_of_equiv`, `CategoryTheory.Cat.leftUnitor_inv_app`, `CategoryTheory.Monoidal.leftUnitor_hom`, `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.Quiv.forget_obj`, `CategoryTheory.Grothendieck.transportIso_hom_fiber`, `CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app`, `CategoryTheory.Pseudofunctor.DescentData.hom_comp`, `CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful`, `CategoryTheory.Cat.Hom.equivFunctor_symm_apply`, `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.Grothendieck.ι_map`, `CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc`, `CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app`, `CategoryTheory.Grothendieck.faithful_ι`, `ContinuousMap.Homotopy.eq_diag_path`, `CategoryTheory.Quiv.equivOfIso_apply`, `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
`coe_mk` 📖	mathematical	—	`α`	—	—

---

← Back to Index