Basic

📁 Source: Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean

Statistics

Metric	Count
Definitions IsUniversal, eta, homMk, homMk', isoMk, map, mapIso, mapNatIso, map₂, map₂IsoPreEquivalenceInverseCompProj, mk, mkIdTerminal, mkPrecomp, post, postIsoMap₂, pre, preEquivalence, functor, inverse, prodEquivalence, prodFunctor, prodInverse, proj, toStructuredArrow, toStructuredArrow', toCostructuredArrow, toCostructuredArrowCompProj, toStructuredArrow, toStructuredArrowCompProj, IsUniversal, desc, eta, homMk, homMk', isoMk, map, mapIso, mapIsoMap₂, mapNatIso, map₂, map₂CompMap₂Iso, map₂IsoPreEquivalenceInverseCompProj, mk, mkIdInitial, mkPostcomp, post, postIsoMap₂, pre, preEquivalence, preEquivalenceFunctor, preEquivalenceInverse, preIsoMap₂, prodEquivalence, prodFunctor, prodInverse, proj, toCostructuredArrow, toCostructuredArrow', costructuredArrowOpEquivalence, instCategoryCostructuredArrow, instCategoryStructuredArrow, structuredArrowOpEquivalence	62
Theorems existsUnique, fac, fac_assoc, hom_desc, hom_ext, uniq, comp_left, epi_homMk, epi_of_epi_left, eqToHom_left, eq_mk, essSurj_map₂, eta_hom_left, eta_inv_left, ext, ext_iff, faithful_map₂, full_map₂, homMk'_comp, homMk'_id, homMk'_left, homMk'_mk_comp, homMk'_mk_id, homMk'_right, homMk_left, homMk_surjective, hom_eq_iff, hom_ext, hom_ext_iff, id_left, instEssSurjCompObjPostOfFull, instEssSurjCompPre, instFaithfulCompObjPost, instFaithfulCompPre, instFullCompObjPostOfFaithful, instFullCompPre, isEquivalenceMap₂, isEquivalence_post, isEquivalence_pre, isoMk_hom_left, isoMk_inv_left, mapIso_counitIso_hom_app_left, mapIso_counitIso_inv_app_left, mapIso_functor_map_left, mapIso_functor_map_right, mapIso_functor_obj_hom, mapIso_functor_obj_left, mapIso_functor_obj_right, mapIso_inverse_map_left, mapIso_inverse_map_right, mapIso_inverse_obj_hom, mapIso_inverse_obj_left, mapIso_inverse_obj_right, mapIso_unitIso_hom_app_left, mapIso_unitIso_inv_app_left, mapNatIso_counitIso_hom_app_left, mapNatIso_counitIso_inv_app_left, mapNatIso_functor_map_left, mapNatIso_functor_map_right, mapNatIso_functor_obj_hom, mapNatIso_functor_obj_left, mapNatIso_functor_obj_right, mapNatIso_inverse_map_left, mapNatIso_inverse_map_right, mapNatIso_inverse_obj_hom, mapNatIso_inverse_obj_left, mapNatIso_inverse_obj_right, mapNatIso_unitIso_hom_app_left, mapNatIso_unitIso_inv_app_left, map_comp, map_id, map_map_left, map_map_right, map_mk, map_obj_hom, map_obj_left, map_obj_right, map₂_map_left, map₂_map_right, map₂_obj_hom, map₂_obj_left, map₂_obj_right, mkPrecomp_comp, mkPrecomp_id, mkPrecomp_left, mkPrecomp_right, mk_hom_eq_self, mk_left, mk_right, mk_surjective, mono_homMk, mono_of_mono_left, obj_ext, post_map, post_obj, functor_map_left, functor_obj_hom, functor_obj_left, functor_obj_right_as, inverse_map_left_left, inverse_obj_hom_left, inverse_obj_left_hom, inverse_obj_left_left, inverse_obj_left_right_as, inverse_obj_right_as, pre_map_left, pre_map_right, pre_obj_hom, pre_obj_left, pre_obj_right, prodEquivalence_counitIso, prodEquivalence_functor, prodEquivalence_inverse, prodEquivalence_unitIso, prodFunctor_map, prodFunctor_obj, prodInverse_map, prodInverse_obj, proj_faithful, proj_map, proj_obj, proj_reflectsIsomorphisms, right_eq_id, toStructuredArrow'_map, toStructuredArrow'_obj, toStructuredArrow_map, toStructuredArrow_obj, w, w_assoc, w_prod_fst, w_prod_fst_assoc, w_prod_snd, w_prod_snd_assoc, toCostructuredArrow_comp_proj, toCostructuredArrow_map, toCostructuredArrow_obj, toStructuredArrow_comp_proj, toStructuredArrow_map, toStructuredArrow_obj, existsUnique, fac, fac_assoc, hom_desc, hom_ext, uniq, comp_right, epi_homMk, epi_of_epi_right, eqToHom_right, eq_mk, essSurj_map₂, eta_hom_right, eta_inv_right, ext, ext_iff, faithful_map₂, full_map₂, homMk'_comp, homMk'_id, homMk'_left, homMk'_mk_comp, homMk'_mk_id, homMk'_right, homMk_right, homMk_surjective, hom_eq_iff, hom_ext, hom_ext_iff, id_right, instEssSurjCompPre, instEssSurjObjCompPostOfFull, instFaithfulCompPre, instFaithfulObjCompPost, instFullCompPre, instFullObjCompPostOfFaithful, isEquivalenceMap₂, isEquivalence_post, isEquivalence_pre, isoMk_hom_right, isoMk_inv_right, left_eq_id, mapIso_counitIso_hom_app_right, mapIso_counitIso_inv_app_right, mapIso_functor_map_left, mapIso_functor_map_right, mapIso_functor_obj_hom, mapIso_functor_obj_left, mapIso_functor_obj_right, mapIso_inverse_map_left, mapIso_inverse_map_right, mapIso_inverse_obj_hom, mapIso_inverse_obj_left, mapIso_inverse_obj_right, mapIso_unitIso_hom_app_right, mapIso_unitIso_inv_app_right, mapNatIso_counitIso_hom_app_right, mapNatIso_counitIso_inv_app_right, mapNatIso_functor_map_left, mapNatIso_functor_map_right, mapNatIso_functor_obj_hom, mapNatIso_functor_obj_left, mapNatIso_functor_obj_right, mapNatIso_inverse_map_left, mapNatIso_inverse_map_right, mapNatIso_inverse_obj_hom, mapNatIso_inverse_obj_left, mapNatIso_inverse_obj_right, mapNatIso_unitIso_hom_app_right, mapNatIso_unitIso_inv_app_right, map_comp, map_id, map_map_left, map_map_right, map_mk, map_obj_hom, map_obj_left, map_obj_right, map₂_map_left, map₂_map_right, map₂_obj_hom, map₂_obj_left, map₂_obj_right, mkPostcomp_comp, mkPostcomp_id, mkPostcomp_left, mkPostcomp_right, mk_hom_eq_self, mk_left, mk_right, mk_surjective, mono_homMk, mono_of_mono_right, obj_ext, post_map, post_obj, preEquivalenceFunctor_map_right, preEquivalenceFunctor_obj_hom, preEquivalenceFunctor_obj_left_as, preEquivalenceFunctor_obj_right, preEquivalenceInverse_map_right_right, preEquivalenceInverse_obj_hom_right, preEquivalenceInverse_obj_left_as, preEquivalenceInverse_obj_right_hom, preEquivalenceInverse_obj_right_left_as, preEquivalenceInverse_obj_right_right, preEquivalence_counitIso, preEquivalence_functor, preEquivalence_inverse, preEquivalence_unitIso, pre_map_left, pre_map_right, pre_obj_hom, pre_obj_left, pre_obj_right, prodEquivalence_counitIso, prodEquivalence_functor, prodEquivalence_inverse, prodEquivalence_unitIso, prodFunctor_map, prodFunctor_obj, prodInverse_map, prodInverse_obj, proj_faithful, proj_map, proj_obj, proj_reflectsIsomorphisms, toCostructuredArrow'_map, toCostructuredArrow'_obj, toCostructuredArrow_map, toCostructuredArrow_obj, w, w_assoc, w_prod_fst, w_prod_fst_assoc, w_prod_snd, w_prod_snd_assoc	276
Total	338

CategoryTheory

Definitions

Name	Category	Theorems
costructuredArrowOpEquivalence 📖	CompOp	—
instCategoryCostructuredArrow 📖	CompOp	437 math math: CostructuredArrow.homMk'_id, Functor.LeftExtension.coconeAtFunctor_map_hom, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit, CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_hom, ObjectProperty.ColimitOfShape.toCostructuredArrow_obj, preservesFiniteLimits_iff_lan_preservesFiniteLimits, TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app, CostructuredArrow.map_comp, CostructuredArrow.toOver_obj_left, OverPresheafAux.costructuredArrowPresheafToOver_map, CategoryOfElements.costructuredArrowYonedaEquivalence_functor, OverPresheafAux.unitAux_hom, Profinite.Extend.cocone_pt, CostructuredArrow.proj_reflectsIsomorphisms, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, CostructuredArrow.ofDiagEquivalence.functor_map_left_left, NonemptyParallelPairPresentationAux.hf, Limits.Cocone.toOver_ι_app, lan_preservesFiniteLimits_of_flat, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, Profinite.Extend.functorOp_map, CostructuredArrow.small_proj_preimage_of_locallySmall, CostructuredArrow.prodEquivalence_counitIso, CostructuredArrow.isEquivalence_pre, OverPresheafAux.restrictedYoneda_map, TwoSquare.structuredArrowRightwardsOpEquivalence_inverse, CostructuredArrow.preEquivalence.functor_obj_right_as, CostructuredArrow.pre_obj_hom, Functor.RightExtension.postcompose₂_obj_left_map, Limits.IsIndObject.isFiltered, OverPresheafAux.restrictedYoneda_obj, Functor.RightExtension.postcompose₂_obj_right, CostructuredArrow.mkPrecomp_id, Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, CostructuredArrow.CreatesConnected.mapCone_raiseCone, CostructuredArrow.mapNatIso_inverse_obj_left, CostructuredArrow.mapIso_functor_obj_hom, CostructuredArrow.functor_obj, CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_hom, CostructuredArrow.toOver_obj_right, TwoSquare.EquivalenceJ.inverse_map, CostructuredArrow.ofDiagEquivalence.inverse_obj_left, Limits.IndObjectPresentation.instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow, Limits.Cocone.toCostructuredArrow_comp_proj, CostructuredArrow.isEquivalenceMap₂, Limits.Cone.fromCostructuredArrow_map_hom, Limits.Cone.toCostructuredArrow_obj, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_right_as, Functor.ι_leftKanExtensionObjIsoColimit_inv, TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, CostructuredArrow.mapNatIso_inverse_map_right, Limits.Cocone.toCostructuredArrow_comp_toOver_comp_forget, CostructuredArrow.unop_left_comp_ofMkLEMk_unop, Functor.RightExtension.postcomp₁_obj_left_map, CostructuredArrow.post_obj, Functor.RightExtension.postcomp₁_map_right, CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, Limits.Cocone.toCostructuredArrow_map, CostructuredArrow.mapNatIso_unitIso_inv_app_left, CostructuredArrow.hasTerminal, CostructuredArrow.prodFunctor_map, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_right, TwoSquare.equivalenceJ_unitIso, CostructuredArrow.map₂_obj_right, CostructuredArrow.mapIso_unitIso_hom_app_left, CostructuredArrow.toOver_map_right, CostructuredArrow.map_obj_hom, LightProfinite.Extend.cocone_ι_app, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app, Condensed.lanPresheafExt_inv, Functor.costructuredArrowMapCocone_pt, CostructuredArrow.toOver_obj_hom, Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, CostructuredArrow.instFullOverToOver, CostructuredArrow.ofDiagEquivalence.functor_obj_hom, CostructuredArrow.homMk'_mk_id, Limits.Cocone.fromCostructuredArrow_ι_app, Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom, Functor.RightExtension.precomp_map_left, Limits.Cocone.toCostructuredArrowCompProj_hom_app, Limits.Cone.fromCostructuredArrow_obj_π, CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_right_as, Functor.ι_leftKanExtensionObjIsoColimit_inv_assoc, CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_hom, OverPresheafAux.counitForward_naturality₁, CostructuredArrow.mapIso_inverse_obj_right, Limits.colimit.toOver_ι_app, CostructuredArrow.costructuredArrowToOverEquivalence.functor_map, isLeftAdjoint_iff_hasTerminal_costructuredArrow, TwoSquare.costructuredArrowRightwards_map, Profinite.Extend.functorOp_obj, CostructuredArrow.ofDiagEquivalence.functor_obj_left_hom, CostructuredArrow.mapIso_functor_map_left, CostructuredArrow.instFaithfulOverToOver, instInitialCostructuredArrowOverToOver, CostructuredArrow.pre_obj_left, CostructuredArrow.post_map, CostructuredArrow.mapIso_unitIso_inv_app_left, CostructuredArrow.essSurj_map₂, CostructuredArrow.map_obj_right, CostructuredArrow.isSeparating_inverseImage_proj, CostructuredArrow.proj_obj, Functor.pointwiseLeftKanExtension_obj, Functor.pointwiseLeftKanExtension_map, IsCardinalAccessibleCategory.final_toCostructuredArrow, CostructuredArrow.preEquivalence.functor_obj_hom, CostructuredArrow.ofCommaFstEquivalence_inverse, CostructuredArrow.mapIso_functor_obj_left, Functor.Initial.out, OverPresheafAux.YonedaCollection.map₂_snd, Limits.Cone.equivCostructuredArrow_inverse, CostructuredArrow.map_obj_left, CostructuredArrow.eta_hom_left, CostructuredArrow.instEssSurjCompPre, CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_hom, TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso, Limits.Cocone.toCostructuredArrowCompToOverCompForget_inv_app, CostructuredArrow.toStructuredArrow'_obj, CostructuredArrow.prodInverse_obj, CostructuredArrow.instEssSurjOverToOver, CostructuredArrow.ofDiagEquivalence.functor_obj_left_left, OverPresheafAux.counitForward_val_snd, CostructuredArrow.initial_post, CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_left, Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso, CostructuredArrow.hasColimitsOfSize, TwoSquare.equivalenceJ_counitIso, CostructuredArrow.id_left, CostructuredArrow.prodEquivalence_inverse, OverPresheafAux.yonedaCollectionFunctor_obj, CostructuredArrow.ofDiagEquivalence.inverse_obj_hom, Functor.RightExtension.coneAtFunctor_obj, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom, CostructuredArrow.map_map_right, CostructuredArrow.closedUnderLimitsOfShape_discrete_empty, Limits.IndObjectPresentation.toCostructuredArrow_obj_right_as, CostructuredArrow.ofCommaFstEquivalenceInverse_obj_right_as, CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_left, IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι, Functor.RightExtension.postcomp₁_obj_left_obj, CostructuredArrow.mapNatIso_functor_obj_hom, CostructuredArrow.CreatesConnected.natTransInCostructuredArrow_app, isCofiltered_costructuredArrow_of_isCofiltered_of_exists, CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso, Functor.toCostructuredArrow_comp_proj, CategoryOfElements.costructuredArrowYonedaEquivalence_inverse, Limits.isIndObject_iff, Presheaf.final_toCostructuredArrow_comp_pre, TwoSquare.instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, CostructuredArrow.proj_faithful, Functor.RightExtension.coneAtWhiskerRightIso_inv_hom, CostructuredArrow.mapNatIso_counitIso_inv_app_left, OverPresheafAux.counitAuxAux_inv, Functor.pointwiseLeftKanExtensionUnit_app, RepresentablyCoflat.filtered, CostructuredArrow.mapIso_counitIso_hom_app_left, Limits.IsIndObject.finallySmall, OverPresheafAux.restrictedYonedaObj_map, CostructuredArrow.epi_homMk, CostructuredArrow.mapCompιCompGrothendieckProj_inv_app, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj, CostructuredArrow.instFullCompPre, CostructuredArrow.isSeparating_proj_preimage, CostructuredArrow.toOver_map_left, Presheaf.tautologicalCocone'_pt, lan_preservesFiniteLimits_of_preservesFiniteLimits, CostructuredArrow.eta_inv_left, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app, CostructuredArrow.instFaithfulCompObjPost, TwoSquare.costructuredArrowDownwardsPrecomp_obj, CategoryOfElements.fromCostructuredArrow_obj_snd, CostructuredArrow.faithful_map₂, CostructuredArrow.mapIso_functor_map_right, CostructuredArrow.functor_map, StructuredArrow.toCostructuredArrow_map, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, OverPresheafAux.counitBackward_counitForward, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, CostructuredArrow.mapNatIso_inverse_map_left, CostructuredArrow.costructuredArrowToOverEquivalence.functor_obj, CostructuredArrow.map₂_map_right, Limits.IndObjectPresentation.toCostructuredArrow_obj_left, TwoSquare.equivalenceJ_inverse, CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_right_as, Limits.Cocone.toOver_pt, CostructuredArrow.pre_obj_right, Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits, Condensed.lanPresheafNatIso_hom_app, CostructuredArrow.CreatesConnected.raiseCone_pt, Limits.IndObjectPresentation.toCostructuredArrow_map_left, Functor.RightExtension.precomp_obj_right, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, CostructuredArrow.toStructuredArrow'_map, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom_assoc, Limits.Cone.toCostructuredArrow_map, CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_right_as, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv_assoc, CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_hom, CostructuredArrow.prodEquivalence_unitIso, CostructuredArrow.full_map₂, Limits.Cocone.toCostructuredArrowCocone_ι_app, Limits.isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits, Functor.initial_iff_isCofiltered_costructuredArrow, CostructuredArrow.mapNatIso_inverse_obj_hom, CostructuredArrow.grothendieckProj_map, Functor.RightExtension.postcomp₁_map_left_app, CostructuredArrow.epi_of_epi_left, CostructuredArrow.mono_of_mono_left, CostructuredArrow.ofCommaFstEquivalence_functor, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, Functor.isDenseAt_iff, Functor.toCostructuredArrow_obj, CostructuredArrow.ofCommaFstEquivalenceFunctor_map_right, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, Functor.LeftExtension.coconeAtFunctor_obj, Limits.IndObjectPresentation.toCostructuredArrow_obj_hom, CostructuredArrow.ofDiagEquivalence.functor_obj_right_as, CostructuredArrow.prodFunctor_obj, Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom, OverPresheafAux.counitAux_hom, CostructuredArrow.mapNatIso_unitIso_hom_app_left, CategoryOfElements.fromCostructuredArrow_map_coe, CostructuredArrow.proj_map, TwoSquare.GuitartExact.isConnected_rightwards, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_map_left_right, CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_left, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_inv_app_app, LightProfinite.Extend.functorOp_map, CostructuredArrow.comp_left, OverPresheafAux.unitAuxAux_inv_app_fst, instInitialCostructuredArrowCompPreOfRepresentablyCoflat, OverPresheafAux.unitAuxAux_inv_app_snd_coe, CostructuredArrow.instEssSurjCompObjPostOfFull, CostructuredArrow.homMk'_mk_comp, CostructuredArrow.preFunctor_app, TwoSquare.structuredArrowRightwardsOpEquivalence_unitIso, CostructuredArrow.ofDiagEquivalence.inverse_obj_right_as, CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_left_left, CostructuredArrow.prodInverse_map, Limits.Cone.equivCostructuredArrow_functor, Functor.PreservesPointwiseRightKanExtensionAt.preserves, CostructuredArrow.instFaithfulCompPre, CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality, CostructuredArrow.toStructuredArrow_obj, Limits.Cocone.fromCostructuredArrow_pt, instIsFilteredCostructuredArrowCompOfRepresentablyCoflat, OverPresheafAux.restrictedYonedaObj_obj, MorphismProperty.instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso, CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_hom, CostructuredArrow.CreatesConnected.raiseCone_π_app, CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso, CostructuredArrow.mapNatIso_functor_obj_left, CostructuredArrow.isoMk_inv_left, OverPresheafAux.restrictedYonedaObjMap₁_app, flat_iff_lan_flat, Functor.RightExtension.postcomp₁_obj_right, CostructuredArrow.ofCommaFstEquivalence_counitIso, Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, CostructuredArrow.hasLimitsOfShape_of_isConnected, CategoryOfElements.toCostructuredArrow_obj, OverPresheafAux.yonedaCollectionFunctor_map, TwoSquare.costructuredArrowDownwardsPrecomp_map, CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_left, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected, OverPresheafAux.YonedaCollection.mk_snd, lan_flat_of_flat, Limits.Cone.equivCostructuredArrow_counitIso, Limits.Cocone.toCostructuredArrowCompToOverCompForget_hom_app, Functor.RightExtension.postcompose₂_obj_hom_app, ObjectProperty.ColimitOfShape.toCostructuredArrow_map, Functor.RightExtension.precomp_obj_hom_app, CostructuredArrow.mapNatIso_functor_obj_right, CostructuredArrow.ofCommaFstEquivalenceFunctor_map_left, Functor.RightExtension.precomp_map_right, CostructuredArrow.map_map_left, CostructuredArrow.map₂_map_left, CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_right, CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app, Functor.RightExtension.postcompose₂ObjMkIso_inv_left_app, OverPresheafAux.YonedaCollection.map₁_comp, CostructuredArrow.preEquivalence.inverse_obj_left_left, CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_left, Functor.RightExtension.postcompose₂_map_left_app, Profinite.Extend.functorOp_final, Functor.RightExtension.postcompose₂_obj_left_obj, CostructuredArrow.ofDiagEquivalence.functor_obj_left_right_as, CostructuredArrow.map_mk, LightCondensed.lanPresheafNatIso_hom_app, TwoSquare.EquivalenceJ.functor_obj, Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, TwoSquare.isConnected_rightwards_iff_downwards, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, Functor.RightExtension.postcompose₂_map_right, Limits.Cone.fromCostructuredArrow_obj_pt, CostructuredArrow.essentiallySmall, LightProfinite.Extend.cocone_pt, CostructuredArrow.mapNatIso_counitIso_hom_app_left, Limits.Cocone.toCostructuredArrow_obj, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, Limits.Cocone.mapCoconeToOver_inv_hom, Functor.LeftExtension.coconeAt_pt, Functor.toCostructuredArrow_map, Profinite.Extend.cocone_ι_app, Functor.RightExtension.coneAtFunctor_map_hom, CostructuredArrow.instFullCompObjPostOfFaithful, Functor.RightExtension.coneAtWhiskerRightIso_hom_hom, CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_right, CostructuredArrow.prodEquivalence_functor, ObjectProperty.isFiltered_costructuredArrow_colimitsCardinalClosure_ι, CostructuredArrow.homMk'_comp, CostructuredArrow.ofDiagEquivalence.inverse_map_left, CostructuredArrow.mapCompιCompGrothendieckProj_hom_app, OverPresheafAux.YonedaCollection.map₁_id, CostructuredArrow.eqToHom_left, CostructuredArrow.mapNatIso_inverse_obj_right, CostructuredArrow.hasColimit, LightCondensed.lanPresheafExt_inv, Condensed.lanPresheafExt_hom, CostructuredArrow.mapNatIso_functor_map_left, TwoSquare.guitartExact_iff_isConnected_rightwards, Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, Presheaf.tautologicalCocone_ι_app, CostructuredArrow.pre_map_right, Presheaf.tautologicalCocone'_ι_app, CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app, CostructuredArrow.hasColimitsOfShape, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, CostructuredArrow.ofCommaFstEquivalence_unitIso, TwoSquare.EquivalenceJ.functor_map, CostructuredArrow.costructuredArrowToOverEquivalence.inverse_obj, Limits.Cocone.toCostructuredArrowCompProj_inv_app, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv, Limits.Cone.equivCostructuredArrow_unitIso, CostructuredArrow.mapIso_functor_obj_right, CostructuredArrow.mono_homMk, CategoryOfElements.fromCostructuredArrow_obj_mk, TwoSquare.equivalenceJ_functor, CostructuredArrow.preEquivalence.inverse_obj_hom_left, CostructuredArrow.preEquivalence.functor_map_left, Functor.RightExtension.postcomp₁_obj_hom_app, Functor.ι_leftKanExtensionObjIsoColimit_hom, CostructuredArrow.isEquivalence_toOver, CostructuredArrow.isClosedUnderColimitsOfShape, CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_right_as, Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, CostructuredArrow.preEquivalence.inverse_obj_right_as, Limits.Cocone.toCostructuredArrowCocone_pt, Functor.LeftExtension.coconeAt_ι_app, CostructuredArrow.IsUniversal.uniq, TwoSquare.guitartExact_iff_final, Limits.IndizationClosedUnderFilteredColimitsAux.isFiltered, TwoSquare.EquivalenceJ.inverse_obj, Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, CostructuredArrow.preEquivalence.inverse_map_left_left, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, OverPresheafAux.counitForward_counitBackward, OverPresheafAux.costructuredArrowPresheafToOver_obj, Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_colimit, CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda, CostructuredArrow.initial_map₂_id, CostructuredArrow.pre_map_left, Limits.Cocone.mapCoconeToOver_hom_hom, Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_hom_app_app, OverPresheafAux.YonedaCollection.map₁_snd, CostructuredArrow.mapNatIso_functor_map_right, Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, CostructuredArrow.mapIso_inverse_obj_hom, CostructuredArrow.mkPrecomp_comp, IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι, TwoSquare.guitartExact_iff_isConnected_downwards, LightCondensed.lanPresheafExt_hom, CostructuredArrow.epi_iff_epi_left, StructuredArrow.toCostructuredArrow'_map, Limits.colimit.toCostructuredArrow_map, CostructuredArrow.preEquivalence.inverse_obj_left_right_as, CostructuredArrow.initial_proj_of_isCofiltered, CostructuredArrow.unop_left_comp_underlyingIso_hom_unop, CostructuredArrow.mapIso_inverse_map_right, StructuredArrow.toCostructuredArrow'_obj, CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_left, instIsCofilteredCostructuredArrowProdDiagOfIsCofilteredOrEmpty, Limits.colimit.toCostructuredArrow_obj, CostructuredArrow.well_copowered_costructuredArrow, CostructuredArrow.map_id, Presheaf.tautologicalCocone_pt, TwoSquare.structuredArrowRightwardsOpEquivalence_functor, Functor.ι_leftKanExtensionObjIsoColimit_hom_assoc, Limits.colimit.toOver_pt, CostructuredArrow.mapIso_inverse_map_left, OverPresheafAux.map_mkPrecomp_eqToHom, CostructuredArrow.map₂_obj_hom, Functor.pointwiseLeftKanExtension_desc_app, CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map, CostructuredArrow.map₂_obj_left, TwoSquare.costructuredArrowRightwards_obj, ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι, Functor.ι_colimitIsoColimitGrothendieck_inv, NonemptyParallelPairPresentationAux.hg, OverPresheafAux.counitAuxAux_hom, CostructuredArrow.ofCommaFstEquivalenceInverse_obj_hom, CostructuredArrow.initial_pre, Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, Functor.RightExtension.postcompose₂ObjMkIso_hom_left_app, CostructuredArrow.projectQuotient_mk, Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right, CostructuredArrow.preEquivalence.functor_obj_left, CostructuredArrow.toStructuredArrow_map, LightProfinite.Extend.functorOp_final, Condensed.lanPresheafIso_hom, CostructuredArrow.isEquivalence_post, CategoryOfElements.fromCostructuredArrow_obj_fst, CostructuredArrow.costructuredArrowToOverEquivalence.inverse_map, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as, CostructuredArrow.mapIso_counitIso_inv_app_left, CostructuredArrow.isoMk_hom_left, Functor.costructuredArrowMapCocone_ι_app, CostructuredArrow.instPreservesLimitsOfShapeProjOfIsConnected, CategoryOfElements.toCostructuredArrow_map, CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app, StructuredArrow.toCostructuredArrow_obj, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc, CostructuredArrow.preEquivalence.inverse_obj_left_hom, CostructuredArrow.small_inverseImage_proj_of_locallySmall, CostructuredArrow.locallySmall, Functor.RightExtension.precomp_obj_left, Functor.instIsEquivalenceRightExtensionCompPrecomp, CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_right, CostructuredArrow.mapIso_inverse_obj_left, OverPresheafAux.counitForward_naturality₂
instCategoryStructuredArrow 📖	CompOp	381 math math: Functor.LeftExtension.coconeAtFunctor_map_hom, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, Limits.Cone.toUnder_pt, StructuredArrow.final_pre, StructuredArrow.projectSubobject_mk, StructuredArrow.instFullUnderToUnder, StructuredArrow.map_map_right, StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left, StructuredArrow.isoMk_inv_right, TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, StructuredArrow.map_comp, StructuredArrow.ofCommaSndEquivalenceFunctor_map_right, Functor.toStructuredArrow_obj, Functor.leftExtensionEquivalenceOfIso₁_functor_map_left, Functor.LeftExtension.precomp₂_obj_hom_app, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right, Limits.limit.toStructuredArrow_obj, StructuredArrow.map_obj_right, StructuredArrow.mapIso_functor_obj_left, CategoryOfElements.fromStructuredArrow_map, Bicategory.LeftLift.whiskering_map, Functor.LeftExtension.precomp₂_map_right, StructuredArrow.commaMapEquivalenceInverse_map, StructuredArrow.ofDiagEquivalence.inverse_map_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, Profinite.Extend.functorOp_map, StructuredArrow.homMk'_comp, StructuredArrow.ofCommaSndEquivalence_functor, StructuredArrow.final_map, CategoryOfElements.structuredArrowEquivalence_functor, StructuredArrow.hasLimit, TwoSquare.structuredArrowRightwardsOpEquivalence_inverse, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as, StructuredArrow.mapIso_inverse_obj_hom, StructuredArrow.toUnder_obj_left, StructuredArrow.IsUniversal.uniq, Functor.pointwiseRightKanExtension_lift_app, CondensedMod.isDiscrete_tfae, Functor.LeftExtension.postcomp₁_map_right_app, StructuredArrow.map₂_obj_right, StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right, Profinite.Extend.cone_π_app, Functor.leftExtensionEquivalenceOfIso₁_functor_obj_left, TwoSquare.EquivalenceJ.inverse_map, StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right, Functor.RightExtension.coneAt_pt, Functor.LeftExtension.postcomp₁_obj_left, StructuredArrow.map₂_map_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_right_as, StructuredArrow.preEquivalenceInverse_obj_right_hom, TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, Functor.LeftExtension.precomp_map_right, Functor.LeftExtension.precomp₂_obj_left, StructuredArrow.proj_faithful, StructuredArrow.ofDiagEquivalence.functor_obj_right_right, Functor.RightExtension.coneAt_π_app, StructuredArrow.mapNatIso_functor_obj_right, StructuredArrow.eta_hom_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_right, Limits.limit.toStructuredArrow_map, TwoSquare.equivalenceJ_unitIso, StructuredArrow.proj_reflectsIsomorphisms, StructuredArrow.prodInverse_map, StructuredArrow.eta_inv_right, Limits.Cone.toStructuredArrowCompProj_inv_app, StructuredArrow.instEssSurjCompPre, StructuredArrow.ofDiagEquivalence.inverse_obj_right, Functor.LeftExtension.precomp_obj_hom_app, CategoryOfElements.to_comma_map_right, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as, StructuredArrow.instEssSurjObjCompPostOfFull, TwoSquare.guitartExact_iff_initial, Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom, Limits.Cone.fromStructuredArrow_π_app, StructuredArrow.id_right, StructuredArrow.final_map₂_id, StructuredArrow.preEquivalenceFunctor_obj_left_as, StructuredArrow.map₂_obj_left, RepresentablyFlat.cofiltered, StructuredArrow.preEquivalence_unitIso, CategoryOfElements.structuredArrowEquivalence_counitIso, Functor.LeftExtension.postcompose₂_obj_right_map, StructuredArrow.functor_map, StructuredArrow.ofCommaSndEquivalence_unitIso, StructuredArrow.map₂_map_left, StructuredArrow.ofCommaSndEquivalence_counitIso, Bicategory.LeftExtension.whiskering_map, StructuredArrow.isEquivalence_pre, StructuredArrow.prodFunctor_map, Functor.leftExtensionEquivalenceOfIso₁_inverse_map_left, Limits.Cone.toStructuredArrowCompToUnderCompForget_hom_app, StructuredArrow.final_post, Functor.Final.out, StructuredArrow.prodEquivalence_functor, Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_left, StructuredArrow.ofDiagEquivalence.inverse_obj_hom, StructuredArrow.mapNatIso_functor_obj_hom, StructuredArrow.mapIso_inverse_obj_right, StructuredArrow.ofDiagEquivalence.functor_obj_right_hom, StructuredArrow.mapNatIso_inverse_map_right, StructuredArrow.prodEquivalence_unitIso, StructuredArrow.full_map₂, isFiltered_structuredArrow_of_isFiltered_of_exists, StructuredArrow.mapNatIso_functor_map_right, StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left, StructuredArrow.mapNatIso_inverse_obj_left, StructuredArrow.ofDiagEquivalence.functor_map_right_right, TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso, CategoryOfElements.toStructuredArrow_obj, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as, StructuredArrow.preEquivalence_inverse, StructuredArrow.preEquivalence_functor, CostructuredArrow.toStructuredArrow'_obj, Limits.Cone.fromStructuredArrow_pt, StructuredArrow.homMk'_mk_comp, Functor.LeftExtension.postcompose₂ObjMkIso_inv_right_app, Limits.Cone.toStructuredArrow_comp_toUnder_comp_forget, StructuredArrow.ofCommaSndEquivalenceFunctor_map_left, TwoSquare.equivalenceJ_counitIso, StructuredArrow.mapNatIso_unitIso_hom_app_right, StructuredArrow.eqToHom_right, Functor.RightExtension.coneAtFunctor_obj, Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right, Functor.toStructuredArrow_map, Functor.LeftExtension.postcompose₂_map_right_app, StructuredArrow.instFaithfulObjCompPost, StructuredArrow.small_inverseImage_proj_of_locallySmall, Limits.Cone.toStructuredArrowCone_π_app, StructuredArrow.mono_iff_mono_right, Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso, Limits.Cocone.toStructuredArrow_obj, StructuredArrow.epi_homMk, Functor.LeftExtension.postcompose₂_obj_hom_app, StructuredArrow.isEquivalence_toUnder, StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right, StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right, instFinalStructuredArrowCompPreOfRepresentablyFlat, LightProfinite.Extend.functor_map, Functor.RightExtension.coneAtWhiskerRightIso_inv_hom, Functor.LeftExtension.postcomp₁_obj_hom_app, CategoryOfElements.fromStructuredArrow_obj, StructuredArrow.ofDiagEquivalence.functor_obj_right_left_as, Limits.Cocone.equivStructuredArrow_unitIso, StructuredArrow.mkPostcomp_comp, Functor.leftExtensionEquivalenceOfIso₁_inverse_map_right, StructuredArrow.isoMk_hom_right, TwoSquare.costructuredArrowDownwardsPrecomp_obj, Functor.LeftExtension.postcompose₂_obj_right_obj, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom, StructuredArrow.toCostructuredArrow_map, StructuredArrow.hasLimitsOfShape, Functor.final_iff_isFiltered_structuredArrow, Limits.Cone.mapConeToUnder_inv_hom, StructuredArrow.toUnder_map_right, TwoSquare.equivalenceJ_inverse, StructuredArrow.isEquivalenceMap₂, Limits.Cocone.fromStructuredArrow_obj_pt, Bicategory.LeftExtension.IsKan.uniqueUpToIso_hom_right, StructuredArrow.isEquivalence_post, Bicategory.HasLeftKanLift.hasInitial, Functor.ranObjObjIsoLimit_inv_π_assoc, CategoryOfElements.structuredArrowEquivalence_inverse, Profinite.Extend.functor_obj, CostructuredArrow.toStructuredArrow'_map, Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_right, MorphismProperty.instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso, StructuredArrow.commaMapEquivalenceInverse_obj, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, StructuredArrow.homMk'_id, Functor.leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom, StructuredArrow.preEquivalenceInverse_obj_right_right, StructuredArrow.preEquivalenceInverse_obj_right_left_as, StructuredArrow.hasLimitsOfSize, Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right, StructuredArrow.mapNatIso_inverse_obj_hom, Functor.LeftExtension.postcompose₂ObjMkIso_hom_right_app, StructuredArrow.commaMapEquivalenceFunctor_obj_left, StructuredArrow.post_map, StructuredArrow.commaMapEquivalenceFunctor_map_left, StructuredArrow.instFaithfulUnderToUnder, Functor.LeftExtension.postcomp₁_obj_right_map, Functor.ranObjObjIsoLimit_hom_π_assoc, Functor.PreservesPointwiseLeftKanExtensionAt.preserves, isRightAdjoint_iff_hasInitial_structuredArrow, StructuredArrow.faithful_map₂, Functor.LeftExtension.coconeAtFunctor_obj, StructuredArrow.pre_map_left, Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom, Functor.instIsEquivalenceLeftExtensionCompPrecomp, Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, TwoSquare.GuitartExact.isConnected_rightwards, StructuredArrow.map_map_left, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_map_left_right, Functor.LeftExtension.precomp_obj_right, StructuredArrow.mapIso_functor_obj_right, StructuredArrow.mapIso_unitIso_inv_app_right, StructuredArrow.prodFunctor_obj, LightProfinite.Extend.functorOp_map, StructuredArrow.proj_map, Functor.LeftExtension.postcompose₂_obj_left, Alexandrov.lowerCone_π_app, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π, Functor.LeftExtension.precomp_obj_left, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right, StructuredArrow.mapIso_functor_map_left, Functor.leftExtensionEquivalenceOfIso₁_functor_obj_hom_app, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right, TwoSquare.structuredArrowRightwardsOpEquivalence_unitIso, StructuredArrow.comp_right, StructuredArrow.commaMapEquivalenceFunctor_map_right, StructuredArrow.essentiallySmall, Limits.Cone.toStructuredArrowCompProj_hom_app, StructuredArrow.map_obj_left, Functor.pointwiseRightKanExtensionCounit_app, StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom, CostructuredArrow.toStructuredArrow_obj, CondensedSet.isDiscrete_tfae, Bicategory.instHasInitialLeftExtensionOfHasLeftKanExtension, Bicategory.LeftExtension.IsKan.uniqueUpToIso_inv_right, Limits.Cocone.fromStructuredArrow_map_hom, Functor.pointwiseRightKanExtension_obj, StructuredArrow.mapNatIso_counitIso_hom_app_right, TwoSquare.costructuredArrowDownwardsPrecomp_map, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected, Functor.LeftExtension.postcompose₂_map_left, Functor.LeftExtension.postcomp₁_obj_right_obj, StructuredArrow.toUnder_obj_hom, StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right, StructuredArrow.map_mk, Limits.Cone.toStructuredArrow_obj, StructuredArrow.mono_homMk, StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right, Bicategory.LeftLift.whiskerOfIdCompIsoSelf_hom_right, instIsCofilteredStructuredArrowCompOfRepresentablyFlat, Bicategory.HasLeftKanExtension.hasInitial, StructuredArrow.preEquivalenceInverse_map_right_right, Functor.Final.zigzag_of_eqvGen_colimitTypeRel, TwoSquare.EquivalenceJ.functor_obj, TwoSquare.isConnected_rightwards_iff_downwards, StructuredArrow.mapIso_unitIso_hom_app_right, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc, Functor.LeftExtension.precomp_map_left, StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right, Limits.Cocone.equivStructuredArrow_inverse, StructuredArrow.pre_map_right, Functor.LeftExtension.precomp₂_obj_right, StructuredArrow.mapIso_functor_obj_hom, StructuredArrow.mapNatIso_unitIso_inv_app_right, Functor.ranObjObjIsoLimit_hom_π, Alexandrov.projSup_obj, StructuredArrow.instFaithfulCompPre, StructuredArrow.functor_obj, Functor.pointwiseRightKanExtension_map, Functor.LeftExtension.postcomp₁_map_left, StructuredArrow.mono_of_mono_right, Functor.RightExtension.coneAtFunctor_map_hom, Alexandrov.lowerCone_pt, Limits.WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, Functor.RightExtension.coneAtWhiskerRightIso_hom_hom, StructuredArrow.mapIso_inverse_map_right, Profinite.Extend.cone_pt, TwoSquare.structuredArrowDownwards_map, Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_hom_right, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π, StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left, StructuredArrow.ofDiagEquivalence.functor_obj_hom, CategoryOfElements.structuredArrowEquivalence_unitIso, Bicategory.LeftLift.IsKan.uniqueUpToIso_hom_right, TwoSquare.structuredArrowDownwards_obj, Limits.Cone.toUnder_π_app, Functor.leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app, TwoSquare.guitartExact_iff_isConnected_rightwards, StructuredArrow.prodEquivalence_inverse, StructuredArrow.ofDiagEquivalence.inverse_obj_left_as, StructuredArrow.mapNatIso_functor_obj_left, StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left, StructuredArrow.preEquivalenceFunctor_map_right, Limits.Cone.toStructuredArrow_comp_proj, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, StructuredArrow.preEquivalenceInverse_obj_hom_right, Bicategory.instHasInitialLeftLiftOfHasLeftKanLift, Limits.Cone.mapConeToUnder_hom_hom, LightProfinite.Extend.functor_initial, Functor.ranObjObjIsoLimit_inv_π, TwoSquare.EquivalenceJ.functor_map, StructuredArrow.mapIso_inverse_obj_left, StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left, StructuredArrow.mapIso_functor_map_right, Functor.structuredArrowMapCone_pt, StructuredArrow.ofCommaSndEquivalence_inverse, StructuredArrow.pre_obj_hom, Limits.Cocone.toStructuredArrow_map, Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right, TwoSquare.equivalenceJ_functor, StructuredArrow.toUnder_map_left, StructuredArrow.prodInverse_obj, Limits.Cone.toStructuredArrow_map, StructuredArrow.preEquivalence_counitIso, StructuredArrow.preEquivalenceInverse_obj_left_as, LightProfinite.Extend.functor_obj, Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_inv_right, StructuredArrow.preEquivalenceFunctor_obj_right, StructuredArrow.proj_obj, Bicategory.LeftLift.IsKan.uniqueUpToIso_inv_right, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as, StructuredArrow.essSurj_map₂, TwoSquare.EquivalenceJ.inverse_obj, StructuredArrow.isCoseparating_proj_preimage, StructuredArrow.map_obj_hom, Functor.LeftExtension.precomp₂_map_left, Bicategory.LeftLift.whiskering_obj, ObjectProperty.LimitOfShape.toStructuredArrow_obj, StructuredArrow.prodEquivalence_counitIso, StructuredArrow.mapIso_inverse_map_left, StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom, StructuredArrow.instEssSurjUnderToUnder, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, Limits.Cone.toStructuredArrowCompToUnderCompForget_inv_app, StructuredArrow.map_id, ObjectProperty.LimitOfShape.toStructuredArrow_map, StructuredArrow.locallySmall, StructuredArrow.instFullCompPre, StructuredArrow.wellPowered_structuredArrow, TwoSquare.guitartExact_iff_isConnected_downwards, Bicategory.LeftExtension.whiskering_obj, StructuredArrow.toCostructuredArrow'_map, StructuredArrow.post_obj, StructuredArrow.toCostructuredArrow'_obj, StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as, Functor.leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app, Bicategory.LeftLift.whiskerOfIdCompIsoSelf_inv_right, TwoSquare.structuredArrowRightwardsOpEquivalence_functor, Limits.Cocone.equivStructuredArrow_functor, instIsFilteredStructuredArrowProdDiagOfIsFilteredOrEmpty, StructuredArrow.mapNatIso_inverse_map_left, Limits.Cocone.fromStructuredArrow_obj_ι, Profinite.Extend.functor_initial, Limits.Cocone.equivStructuredArrow_counitIso, Limits.Cone.toStructuredArrowCone_pt, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc, StructuredArrow.instFullObjCompPostOfFaithful, StructuredArrow.ofDiagEquivalence.functor_obj_left_as, Profinite.Extend.functor_map, StructuredArrow.toUnder_obj_right, Functor.toStructuredArrow_comp_proj, StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right, StructuredArrow.mapNatIso_functor_map_left, StructuredArrow.map₂_obj_hom, StructuredArrow.mapNatIso_counitIso_inv_app_right, StructuredArrow.commaMapEquivalenceFunctor_obj_right, Functor.leftExtensionEquivalenceOfIso₁_functor_map_right, StructuredArrow.isCoseparating_inverseImage_proj, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom, CostructuredArrow.toStructuredArrow_map, StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom, Functor.leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app, StructuredArrow.homMk'_mk_id, Alexandrov.projSup_map, StructuredArrow.pre_obj_left, StructuredArrow.epi_of_epi_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as, StructuredArrow.mkPostcomp_id, StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right, StructuredArrow.mapIso_counitIso_hom_app_right, StructuredArrow.toCostructuredArrow_obj, StructuredArrow.final_proj_of_isFiltered, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom, StructuredArrow.mapNatIso_inverse_obj_right, StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right, StructuredArrow.preEquivalenceFunctor_obj_hom, StructuredArrow.mapIso_counitIso_inv_app_right, Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right, StructuredArrow.commaMapEquivalenceFunctor_obj_hom, StructuredArrow.pre_obj_right, StructuredArrow.small_proj_preimage_of_locallySmall, Functor.leftExtensionEquivalenceOfIso₁_functor_obj_right, Functor.structuredArrowMapCone_π_app
structuredArrowOpEquivalence 📖	CompOp	—

CategoryTheory.CostructuredArrow

Definitions

Name	Category	Theorems
IsUniversal 📖	CompOp	1 math math: CategoryTheory.Functor.IsRightKanExtension.nonempty_isUniversal
eta 📖	CompOp	3 math math: eta_hom_left, eta_inv_left, CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso
homMk 📖	CompOp	33 math math: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver_map, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, Profinite.Extend.functorOp_map, CategoryTheory.TwoSquare.EquivalenceJ.inverse_map, CategoryTheory.Limits.Cocone.toCostructuredArrow_map, prodFunctor_map, commaToGrothendieckPrecompFunctor_map_fiber, costructuredArrowToOverEquivalence.functor_map, CategoryTheory.TwoSquare.costructuredArrowRightwards_map, post_map, epi_homMk, CategoryTheory.StructuredArrow.toCostructuredArrow_map, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, CategoryTheory.Limits.Cone.toCostructuredArrow_map, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, LightProfinite.Extend.functorOp_map, homMk_left, prodInverse_map, CreatesConnected.raiseCone_π_app, CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_map, CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map, CategoryTheory.Functor.toCostructuredArrow_map, CategoryTheory.TwoSquare.EquivalenceJ.functor_map, mono_homMk, CategoryTheory.TwoSquare.EquivalenceJ.inverse_obj, preEquivalence.inverse_map_left_left, CategoryTheory.StructuredArrow.toCostructuredArrow'_map, CategoryTheory.Limits.colimit.toCostructuredArrow_map, homMk_surjective, costructuredArrowToOverEquivalence.inverse_map, CategoryTheory.CategoryOfElements.toCostructuredArrow_map
homMk' 📖	CompOp	6 math math: homMk'_id, homMk'_mk_id, homMk'_right, homMk'_left, homMk'_mk_comp, homMk'_comp
isoMk 📖	CompOp	4 math math: CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, isoMk_inv_left, isoMk_hom_left
map 📖	CompOp	20 math math: map_comp, CategoryTheory.NonemptyParallelPairPresentationAux.hf, map_obj_hom, map_obj_right, CategoryTheory.Functor.pointwiseLeftKanExtension_map, map_obj_left, map_map_right, mapCompιCompGrothendieckProj_inv_app, functor_map, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app, grothendieckProj_map, CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality, map_map_left, map_mk, mapCompιCompGrothendieckProj_hom_app, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, map_id, CategoryTheory.NonemptyParallelPairPresentationAux.hg
mapIso 📖	CompOp	14 math math: mapIso_functor_obj_hom, mapIso_unitIso_hom_app_left, mapIso_inverse_obj_right, mapIso_functor_map_left, mapIso_unitIso_inv_app_left, mapIso_functor_obj_left, mapIso_counitIso_hom_app_left, mapIso_functor_map_right, mapIso_functor_obj_right, mapIso_inverse_obj_hom, mapIso_inverse_map_right, mapIso_inverse_map_left, mapIso_counitIso_inv_app_left, mapIso_inverse_obj_left
mapNatIso 📖	CompOp	14 math math: mapNatIso_inverse_obj_left, mapNatIso_inverse_map_right, mapNatIso_unitIso_inv_app_left, mapNatIso_functor_obj_hom, mapNatIso_counitIso_inv_app_left, mapNatIso_inverse_map_left, mapNatIso_inverse_obj_hom, mapNatIso_unitIso_hom_app_left, mapNatIso_functor_obj_left, mapNatIso_functor_obj_right, mapNatIso_counitIso_hom_app_left, mapNatIso_inverse_obj_right, mapNatIso_functor_map_left, mapNatIso_functor_map_right
map₂ 📖	CompOp	10 math math: isEquivalenceMap₂, map₂_obj_right, essSurj_map₂, faithful_map₂, map₂_map_right, full_map₂, map₂_map_left, initial_map₂_id, map₂_obj_hom, map₂_obj_left
map₂IsoPreEquivalenceInverseCompProj 📖	CompOp	—
mk 📖	CompOp	—
mkIdTerminal 📖	CompOp	—
mkPrecomp 📖	CompOp	6 math math: mkPrecomp_id, mkPrecomp_left, mkPrecomp_right, CategoryTheory.OverPresheafAux.YonedaCollection.map₂_snd, mkPrecomp_comp, CategoryTheory.OverPresheafAux.map_mkPrecomp_eqToHom
post 📖	CompOp	9 math math: post_obj, post_map, initial_post, instFaithfulCompObjPost, instEssSurjCompObjPostOfFull, CategoryTheory.TwoSquare.EquivalenceJ.functor_obj, instFullCompObjPostOfFaithful, CategoryTheory.TwoSquare.EquivalenceJ.functor_map, isEquivalence_post
postIsoMap₂ 📖	CompOp	—
pre 📖	CompOp	29 math math: CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, isEquivalence_pre, preEquivalence.functor_obj_right_as, pre_obj_hom, CategoryTheory.TwoSquare.costructuredArrowRightwards_map, pre_obj_left, preEquivalence.functor_obj_hom, instEssSurjCompPre, CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre, instFullCompPre, pre_obj_right, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_map_left, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app, CategoryTheory.instInitialCostructuredArrowCompPreOfRepresentablyCoflat, preFunctor_app, instFaithfulCompPre, preEquivalence.inverse_obj_left_left, pre_map_right, preEquivalence.inverse_obj_hom_left, preEquivalence.functor_map_left, preEquivalence.inverse_obj_right_as, CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt, preEquivalence.inverse_map_left_left, pre_map_left, preEquivalence.inverse_obj_left_right_as, CategoryTheory.TwoSquare.costructuredArrowRightwards_obj, initial_pre, preEquivalence.functor_obj_left, preEquivalence.inverse_obj_left_hom
preEquivalence 📖	CompOp	—
prodEquivalence 📖	CompOp	4 math math: prodEquivalence_counitIso, prodEquivalence_inverse, prodEquivalence_unitIso, prodEquivalence_functor
prodFunctor 📖	CompOp	5 math math: prodEquivalence_counitIso, prodFunctor_map, prodEquivalence_unitIso, prodFunctor_obj, prodEquivalence_functor
prodInverse 📖	CompOp	5 math math: prodEquivalence_counitIso, prodInverse_obj, prodEquivalence_inverse, prodEquivalence_unitIso, prodInverse_map
proj 📖	CompOp	107 math math: CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom, CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits, LightCondensed.lanPresheafIso_hom, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app, Profinite.Extend.cocone_pt, proj_reflectsIsomorphisms, ofDiagEquivalence.functor_map_left_left, CategoryTheory.lan_preservesFiniteLimits_of_flat, small_proj_preimage_of_locallySmall, CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, CreatesConnected.mapCone_raiseCone, ofCostructuredArrowProjEquivalence.inverse_obj_left_hom, CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_proj, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv, LightProfinite.Extend.cocone_ι_app, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_inv_app_app, Condensed.lanPresheafExt_inv, CategoryTheory.Functor.costructuredArrowMapCocone_pt, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, CategoryTheory.Limits.Cocone.fromCostructuredArrow_ι_app, CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom, CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_hom_app, ofCostructuredArrowProjEquivalence.functor_obj_right_as, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv_assoc, ιCompGrothendieckProj_inv_app, ofCostructuredArrowProjEquivalence.inverse_obj_hom, isSeparating_inverseImage_proj, proj_obj, CategoryTheory.Functor.pointwiseLeftKanExtension_obj, CategoryTheory.Functor.pointwiseLeftKanExtension_map, ofCostructuredArrowProjEquivalence.inverse_map_left_left, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom, ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, CreatesConnected.natTransInCostructuredArrow_app, CategoryTheory.Functor.toCostructuredArrow_comp_proj, proj_faithful, CategoryTheory.Functor.pointwiseLeftKanExtensionUnit_app, mapCompιCompGrothendieckProj_inv_app, isSeparating_proj_preimage, CategoryTheory.Presheaf.tautologicalCocone'_pt, CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso_hom_app_app, ofCostructuredArrowProjEquivalence.functor_obj_left_right_as, Condensed.lanPresheafNatIso_hom_app, CreatesConnected.raiseCone_pt, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom_assoc, ofCostructuredArrowProjEquivalence.inverse_obj_right_as, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv_assoc, ofCostructuredArrowProjEquivalence.functor_obj_left_hom, CategoryTheory.Functor.isDenseAt_iff, CategoryTheory.Functor.LeftExtension.coconeAtFunctor_obj, CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom, proj_map, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_inv_app_app, ofCostructuredArrowProjEquivalence.functor_map_left_left, CategoryTheory.Limits.Cocone.fromCostructuredArrow_pt, ofCostructuredArrowProjEquivalence.functor_obj_hom, CreatesConnected.raiseCone_π_app, CategoryTheory.flat_iff_lan_flat, CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, CategoryTheory.lan_flat_of_flat, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app, ofCostructuredArrowProjEquivalence.functor_obj_left_left, LightCondensed.lanPresheafNatIso_hom_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, LightProfinite.Extend.cocone_pt, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, CategoryTheory.Functor.LeftExtension.coconeAt_pt, Profinite.Extend.cocone_ι_app, ofDiagEquivalence.inverse_map_left, mapCompιCompGrothendieckProj_hom_app, LightCondensed.lanPresheafExt_inv, Condensed.lanPresheafExt_hom, ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, CategoryTheory.Presheaf.tautologicalCocone_ι_app, CategoryTheory.Presheaf.tautologicalCocone'_ι_app, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app, CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_inv_app, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom, ofCostructuredArrowProjEquivalence.inverse_obj_left_right_as, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, CategoryTheory.Functor.LeftExtension.coconeAt_ι_app, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, ιCompGrothendieckProj_hom_app, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_hom_app_app, CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, LightCondensed.lanPresheafExt_hom, initial_proj_of_isCofiltered, ofCostructuredArrowProjEquivalence.inverse_obj_left_left, CategoryTheory.Presheaf.tautologicalCocone_pt, CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom_assoc, CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, CategoryTheory.MonoidalCategory.DayFunctor.η_comp_isoPointwiseLeftKanExtension_hom, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right, Condensed.lanPresheafIso_hom, CategoryTheory.MonoidalCategory.DayFunctor.ι_comp_isoPointwiseLeftKanExtension_inv, CategoryTheory.Functor.costructuredArrowMapCocone_ι_app, instPreservesLimitsOfShapeProjOfIsConnected, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc, small_inverseImage_proj_of_locallySmall
toStructuredArrow 📖	CompOp	2 math math: toStructuredArrow_obj, toStructuredArrow_map
toStructuredArrow' 📖	CompOp	2 math math: toStructuredArrow'_obj, toStructuredArrow'_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.CostructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Comma.left	—	—
epi_homMk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom	CategoryTheory.Epi CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow homMk	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful proj_faithful
epi_of_epi_left 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful proj_faithful
eqToHom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.eqToHom CategoryTheory.CostructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Comma.left	—	—
eq_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—
essSurj_map₂ 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	CategoryTheory.Comma.essSurj_map CategoryTheory.Functor.instEssSurjId CategoryTheory.Discrete.instIsIsoFunctorNatTrans
eta_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Iso.hom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
eta_inv_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—	CategoryTheory.CommaMorphism.ext CategoryTheory.Discrete.instSubsingletonDiscreteHom
ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	ext
faithful_map₂ 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	CategoryTheory.Comma.faithful_map CategoryTheory.Functor.Faithful.id
full_map₂ 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	CategoryTheory.Comma.full_map CategoryTheory.Functor.Full.id CategoryTheory.Discrete.instIsIsoFunctorNatTrans
homMk'_comp 📖	mathematical	—	homMk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.instCategoryCostructuredArrow CategoryTheory.eqToHom	—	eqToHom_left CategoryTheory.Category.id_comp
homMk'_id 📖	mathematical	—	homMk' CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.CostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	eqToHom_left
homMk'_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.map CategoryTheory.Comma.hom homMk'	—	—
homMk'_mk_comp 📖	mathematical	—	homMk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Comma.hom CategoryTheory.eqToHom	—	homMk'_comp
homMk'_mk_id 📖	mathematical	—	homMk' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.CostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.left CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	homMk'_id
homMk'_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Functor.map CategoryTheory.Comma.hom homMk' CategoryTheory.CategoryStruct.id	—	—
homMk_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left homMk	—	—
homMk_surjective 📖	mathematical	—	homMk	—	w
hom_eq_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	hom_ext
hom_ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—	CategoryTheory.CommaMorphism.ext CategoryTheory.Discrete.instSubsingletonDiscreteHom
hom_ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	hom_ext
id_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.id CategoryTheory.CostructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Comma.left	—	—
instEssSurjCompObjPostOfFull 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.instCategoryCostructuredArrow post	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_preimage
instEssSurjCompPre 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	CategoryTheory.Comma.instEssSurjCompPreLeft
instFaithfulCompObjPost 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.obj post	—	—
instFaithfulCompPre 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	CategoryTheory.Comma.instFaithfulCompPreLeft
instFullCompObjPostOfFaithful 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.obj post	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Discrete.functor_map_id CategoryTheory.Category.comp_id CategoryTheory.CommaMorphism.w
instFullCompPre 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	CategoryTheory.Comma.instFullCompPreLeft
isEquivalenceMap₂ 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	CategoryTheory.Comma.isEquivalenceMap CategoryTheory.Functor.isEquivalence_refl CategoryTheory.Discrete.instIsIsoFunctorNatTrans
isEquivalence_post 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.obj post	—	instFaithfulCompObjPost instFullCompObjPostOfFaithful instEssSurjCompObjPostOfFull
isEquivalence_pre 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	CategoryTheory.Comma.isEquivalence_preLeft
isoMk_hom_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow isoMk	—	—
isoMk_inv_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow isoMk	—	—
mapIso_counitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.hom CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapIso_counitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.hom CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapIso_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso	—	—
mapIso_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.id	—	—
mapIso_functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Iso.hom	—	—
mapIso_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso	—	—
mapIso_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso	—	—
mapIso_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso	—	—
mapIso_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.id	—	—
mapIso_inverse_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Iso.inv	—	—
mapIso_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso	—	—
mapIso_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso	—	—
mapIso_unitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.inv CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapIso_unitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.inv CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapNatIso_counitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapNatIso_counitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapNatIso_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso	—	—
mapNatIso_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.id	—	—
mapNatIso_functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapNatIso_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso	—	—
mapNatIso_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso	—	—
mapNatIso_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso	—	—
mapNatIso_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.id	—	—
mapNatIso_inverse_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapNatIso_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso	—	—
mapNatIso_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso	—	—
mapNatIso_unitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapNatIso_unitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
map_comp 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc
map_id 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
map_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map	—	—
map_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map CategoryTheory.CategoryStruct.id	—	—
map_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
map_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
map_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map	—	—
map_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map	—	—
map₂_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	—
map₂_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂ CategoryTheory.CategoryStruct.id	—	—
map₂_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.map	—	—
map₂_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	—
map₂_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map₂	—	—
mkPrecomp_comp 📖	mathematical	—	mkPrecomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.eqToHom	—	eqToHom_left CategoryTheory.Category.id_comp
mkPrecomp_id 📖	mathematical	—	mkPrecomp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	eqToHom_left
mkPrecomp_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map mkPrecomp	—	—
mkPrecomp_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map mkPrecomp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mk_hom_eq_self 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mk_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mk_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mk_surjective 📖	—	—	—	—	—
mono_homMk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom	CategoryTheory.Mono CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow homMk	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful proj_faithful
mono_of_mono_left 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful proj_faithful
obj_ext 📖	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.Comma.hom	—	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
post_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.obj post homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left	—	—
post_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp post CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
pre_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow pre	—	—
pre_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow pre CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
pre_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	—
pre_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	—
pre_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow pre	—	—
prodEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryCostructuredArrow prodEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp prodInverse prodFunctor CategoryTheory.Functor.id CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
prodEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryCostructuredArrow prodEquivalence prodFunctor	—	—
prodEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryCostructuredArrow prodEquivalence prodInverse	—	—
prodEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryCostructuredArrow prodEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp prodFunctor prodInverse CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
prodFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryCostructuredArrow prodFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom homMk CategoryTheory.CommaMorphism.left	—	—
prodFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryCostructuredArrow prodFunctor CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
prodInverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.prod prodInverse homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left	—	—
prodInverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.prod' CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.prod prodInverse CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom	—	—
proj_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow proj	—	ext
proj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow proj CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
proj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow proj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
proj_reflectsIsomorphisms 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow proj	—	CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.IsIso.inv_comp_eq CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id hom_ext CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsIso.inv_hom_id
right_eq_id 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
toStructuredArrow'_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.Functor.op Opposite.op CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow' CategoryTheory.StructuredArrow.homMk Opposite.unop CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left	—	—
toStructuredArrow'_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.Functor.op Opposite.op CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow' Opposite.unop CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
toStructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow Opposite.op CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left Quiver.Hom.unop	—	—
toStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.StructuredArrow Opposite.op CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w
w_prod_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.prod' CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.prod CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom	—	w
w_prod_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.prod' CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.prod CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CommaMorphism.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w_prod_fst
w_prod_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.prod' CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.prod CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom	—	w
w_prod_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.prod' CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.prod CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CommaMorphism.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w_prod_snd

CategoryTheory.CostructuredArrow.IsUniversal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsUnique 📖	mathematical	—	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	fac hom_ext
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map lift CategoryTheory.Comma.hom	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map lift CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hom_desc 📖	mathematical	—	lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	CategoryTheory.Limits.IsTerminal.hom_ext
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—	hom_desc
uniq 📖	mathematical	—	CategoryTheory.Limits.IsTerminal.from CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.Limits.IsTerminal.hom_ext

CategoryTheory.CostructuredArrow.preEquivalence

Definitions

Name	Category	Theorems
functor 📖	CompOp	4 math math: functor_obj_right_as, functor_obj_hom, functor_map_left, functor_obj_left
inverse 📖	CompOp	6 math math: inverse_obj_left_left, inverse_obj_hom_left, inverse_obj_right_as, inverse_map_left_left, inverse_obj_left_right_as, inverse_obj_left_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map functor	—	—
functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre functor CategoryTheory.CommaMorphism.left	—	—
functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre functor	—	—
functor_obj_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre functor	—	—
inverse_map_left_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.CostructuredArrow.homMk inverse	—	—
inverse_obj_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Comma.right CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Comma.hom inverse	—	—
inverse_obj_left_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre inverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	—	—
inverse_obj_left_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre inverse	—	—
inverse_obj_left_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre inverse	—	—
inverse_obj_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.CostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre CategoryTheory.Comma.left inverse	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
toCostructuredArrow 📖	CompOp	4 math math: CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_left, toCostructuredArrow_comp_proj, toCostructuredArrow_obj, toCostructuredArrow_map
toCostructuredArrowCompProj 📖	CompOp	—
toStructuredArrow 📖	CompOp	4 math math: toStructuredArrow_obj, toStructuredArrow_map, CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right, toStructuredArrow_comp_proj
toStructuredArrowCompProj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCostructuredArrow_comp_proj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map	comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.proj	—	—
toCostructuredArrow_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map	CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk	—	—
toCostructuredArrow_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map	CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow	—	—
toStructuredArrow_comp_proj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map	comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.proj	—	—
toStructuredArrow_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map	CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.homMk	—	—
toStructuredArrow_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map	CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow	—	—

CategoryTheory.StructuredArrow

Definitions

Name	Category	Theorems
IsUniversal 📖	CompOp	1 math math: CategoryTheory.Functor.IsLeftKanExtension.nonempty_isUniversal
eta 📖	CompOp	3 math math: eta_hom_right, eta_inv_right, CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso
homMk 📖	CompOp	31 math math: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, commaMapEquivalenceInverse_map, Profinite.Extend.functorOp_map, CategoryTheory.TwoSquare.EquivalenceJ.inverse_map, CategoryTheory.Limits.limit.toStructuredArrow_map, prodInverse_map, prodFunctor_map, CategoryTheory.Functor.toStructuredArrow_map, CategoryTheory.Limits.Cone.toStructuredArrowCone_π_app, epi_homMk, LightProfinite.Extend.functor_map, homMk_right, CategoryTheory.CostructuredArrow.toStructuredArrow'_map, post_map, commaMapEquivalenceFunctor_map_left, LightProfinite.Extend.functorOp_map, commaMapEquivalenceFunctor_map_right, CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp_map, mono_homMk, preEquivalenceInverse_map_right_right, CategoryTheory.TwoSquare.EquivalenceJ.functor_obj, CategoryTheory.TwoSquare.structuredArrowDownwards_map, CategoryTheory.TwoSquare.EquivalenceJ.functor_map, CategoryTheory.Limits.Cocone.toStructuredArrow_map, CategoryTheory.Limits.Cone.toStructuredArrow_map, CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map, Profinite.Extend.functor_map, CategoryTheory.CostructuredArrow.toStructuredArrow_map, homMk_surjective, commaMapEquivalenceFunctor_obj_hom
homMk' 📖	CompOp	6 math math: homMk'_comp, homMk'_mk_comp, homMk'_left, homMk'_id, homMk'_right, homMk'_mk_id
isoMk 📖	CompOp	4 math math: isoMk_inv_right, preEquivalence_unitIso, isoMk_hom_right, preEquivalence_counitIso
map 📖	CompOp	15 math math: map_map_right, map_comp, map_obj_right, CategoryTheory.Functor.LeftExtension.precomp₂_map_right, final_map, functor_map, CategoryTheory.Limits.Cone.toStructuredArrowCone_π_app, map_map_left, map_obj_left, map_mk, CategoryTheory.Functor.pointwiseRightKanExtension_map, map_obj_hom, CategoryTheory.Functor.LeftExtension.precomp₂_map_left, map_id, CategoryTheory.Limits.Cone.toStructuredArrowCone_pt
mapIso 📖	CompOp	14 math math: mapIso_functor_obj_left, mapIso_inverse_obj_hom, mapIso_inverse_obj_right, mapIso_functor_obj_right, mapIso_unitIso_inv_app_right, mapIso_functor_map_left, mapIso_unitIso_hom_app_right, mapIso_functor_obj_hom, mapIso_inverse_map_right, mapIso_inverse_obj_left, mapIso_functor_map_right, mapIso_inverse_map_left, mapIso_counitIso_hom_app_right, mapIso_counitIso_inv_app_right
mapIsoMap₂ 📖	CompOp	—
mapNatIso 📖	CompOp	14 math math: mapNatIso_functor_obj_right, mapNatIso_functor_obj_hom, mapNatIso_inverse_map_right, mapNatIso_functor_map_right, mapNatIso_inverse_obj_left, mapNatIso_unitIso_hom_app_right, mapNatIso_inverse_obj_hom, mapNatIso_counitIso_hom_app_right, mapNatIso_unitIso_inv_app_right, mapNatIso_functor_obj_left, mapNatIso_inverse_map_left, mapNatIso_functor_map_left, mapNatIso_counitIso_inv_app_right, mapNatIso_inverse_obj_right
map₂ 📖	CompOp	25 math math: commaMapEquivalenceInverse_map, map₂_obj_right, commaMapEquivalenceCounitIso_hom_app_left_right, commaMapEquivalenceUnitIso_inv_app_right_right, map₂_map_right, final_map₂_id, map₂_obj_left, map₂_map_left, full_map₂, isEquivalenceMap₂, commaMapEquivalenceInverse_obj, commaMapEquivalenceFunctor_obj_left, commaMapEquivalenceFunctor_map_left, faithful_map₂, commaMapEquivalenceFunctor_map_right, commaMapEquivalenceCounitIso_hom_app_right_right, commaMapEquivalenceUnitIso_hom_app_right_right, commaMapEquivalenceUnitIso_hom_app_right_left, commaMapEquivalenceUnitIso_inv_app_right_left, essSurj_map₂, commaMapEquivalenceCounitIso_inv_app_left_right, map₂_obj_hom, commaMapEquivalenceFunctor_obj_right, commaMapEquivalenceCounitIso_inv_app_right_right, commaMapEquivalenceFunctor_obj_hom
map₂CompMap₂Iso 📖	CompOp	—
map₂IsoPreEquivalenceInverseCompProj 📖	CompOp	—
mk 📖	CompOp	—
mkIdInitial 📖	CompOp	—
mkPostcomp 📖	CompOp	4 math math: mkPostcomp_left, mkPostcomp_comp, mkPostcomp_right, mkPostcomp_id
post 📖	CompOp	9 math math: CategoryTheory.TwoSquare.EquivalenceJ.inverse_map, instEssSurjObjCompPostOfFull, final_post, instFaithfulObjCompPost, isEquivalence_post, post_map, CategoryTheory.TwoSquare.EquivalenceJ.inverse_obj, post_obj, instFullObjCompPostOfFaithful
postIsoMap₂ 📖	CompOp	—
pre 📖	CompOp	29 math math: final_pre, preEquivalenceInverse_obj_right_hom, instEssSurjCompPre, preEquivalenceFunctor_obj_left_as, preEquivalence_unitIso, isEquivalence_pre, preEquivalence_inverse, preEquivalence_functor, CategoryTheory.Limits.Cone.toStructuredArrowCone_π_app, CategoryTheory.instFinalStructuredArrowCompPreOfRepresentablyFlat, preEquivalenceInverse_obj_right_right, preEquivalenceInverse_obj_right_left_as, pre_map_left, preEquivalenceInverse_map_right_right, pre_map_right, instFaithfulCompPre, CategoryTheory.TwoSquare.structuredArrowDownwards_map, CategoryTheory.TwoSquare.structuredArrowDownwards_obj, preEquivalenceFunctor_map_right, preEquivalenceInverse_obj_hom_right, pre_obj_hom, preEquivalence_counitIso, preEquivalenceInverse_obj_left_as, preEquivalenceFunctor_obj_right, instFullCompPre, CategoryTheory.Limits.Cone.toStructuredArrowCone_pt, pre_obj_left, preEquivalenceFunctor_obj_hom, pre_obj_right
preEquivalence 📖	CompOp	4 math math: preEquivalence_unitIso, preEquivalence_inverse, preEquivalence_functor, preEquivalence_counitIso
preEquivalenceFunctor 📖	CompOp	7 math math: preEquivalenceFunctor_obj_left_as, preEquivalence_unitIso, preEquivalence_functor, preEquivalenceFunctor_map_right, preEquivalence_counitIso, preEquivalenceFunctor_obj_right, preEquivalenceFunctor_obj_hom
preEquivalenceInverse 📖	CompOp	9 math math: preEquivalenceInverse_obj_right_hom, preEquivalence_unitIso, preEquivalence_inverse, preEquivalenceInverse_obj_right_right, preEquivalenceInverse_obj_right_left_as, preEquivalenceInverse_map_right_right, preEquivalenceInverse_obj_hom_right, preEquivalence_counitIso, preEquivalenceInverse_obj_left_as
preIsoMap₂ 📖	CompOp	—
prodEquivalence 📖	CompOp	4 math math: prodEquivalence_functor, prodEquivalence_unitIso, prodEquivalence_inverse, prodEquivalence_counitIso
prodFunctor 📖	CompOp	5 math math: prodFunctor_map, prodEquivalence_functor, prodEquivalence_unitIso, prodFunctor_obj, prodEquivalence_counitIso
prodInverse 📖	CompOp	5 math math: prodInverse_map, prodEquivalence_unitIso, prodEquivalence_inverse, prodInverse_obj, prodEquivalence_counitIso
proj 📖	CompOp	56 math math: CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, ofStructuredArrowProjEquivalence.inverse_obj_right_right, ofDiagEquivalence.inverse_map_right, ofStructuredArrowProjEquivalence.inverse_obj_right_left_as, CategoryTheory.Functor.pointwiseRightKanExtension_lift_app, Profinite.Extend.cone_π_app, CategoryTheory.Functor.RightExtension.coneAt_pt, proj_faithful, CategoryTheory.Functor.RightExtension.coneAt_π_app, proj_reflectsIsomorphisms, CategoryTheory.Limits.Cone.toStructuredArrowCompProj_inv_app, ofStructuredArrowProjEquivalence.functor_obj_left_as, CategoryTheory.Limits.Cone.fromStructuredArrow_π_app, ofDiagEquivalence.functor_map_right_right, ofStructuredArrowProjEquivalence.inverse_obj_left_as, CategoryTheory.Limits.Cone.fromStructuredArrow_pt, CategoryTheory.Functor.RightExtension.coneAtFunctor_obj, small_inverseImage_proj_of_locallySmall, ofStructuredArrowProjEquivalence.functor_map_right_right, CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_inv_hom, ofStructuredArrowProjEquivalence.functor_obj_right_hom, CategoryTheory.Functor.ranObjObjIsoLimit_inv_π_assoc, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, ofStructuredArrowProjEquivalence.inverse_obj_hom, CategoryTheory.Functor.ranObjObjIsoLimit_hom_π_assoc, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, proj_map, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π, ofStructuredArrowProjEquivalence.functor_obj_right_right, ofStructuredArrowProjEquivalence.inverse_map_right_right, CategoryTheory.Limits.Cone.toStructuredArrowCompProj_hom_app, CategoryTheory.Functor.pointwiseRightKanExtensionCounit_app, CategoryTheory.Functor.pointwiseRightKanExtension_obj, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc, CategoryTheory.Functor.ranObjObjIsoLimit_hom_π, CategoryTheory.Functor.pointwiseRightKanExtension_map, CategoryTheory.Functor.RightExtension.coneAtFunctor_map_hom, CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_hom_hom, Profinite.Extend.cone_pt, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π, CategoryTheory.Limits.Cone.toStructuredArrow_comp_proj, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, CategoryTheory.Functor.ranObjObjIsoLimit_inv_π, CategoryTheory.Functor.structuredArrowMapCone_pt, proj_obj, ofStructuredArrowProjEquivalence.functor_obj_right_left_as, isCoseparating_proj_preimage, CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc, CategoryTheory.Functor.toStructuredArrow_comp_proj, isCoseparating_inverseImage_proj, ofStructuredArrowProjEquivalence.inverse_obj_right_hom, final_proj_of_isFiltered, ofStructuredArrowProjEquivalence.functor_obj_hom, small_proj_preimage_of_locallySmall, CategoryTheory.Functor.structuredArrowMapCone_π_app
toCostructuredArrow 📖	CompOp	2 math math: toCostructuredArrow_map, toCostructuredArrow_obj
toCostructuredArrow' 📖	CompOp	2 math math: toCostructuredArrow'_map, toCostructuredArrow'_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.StructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryStructuredArrow CategoryTheory.Comma.right	—	—
epi_homMk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map	CategoryTheory.Epi CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow homMk	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful proj_faithful
epi_of_epi_right 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful proj_faithful
eqToHom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.eqToHom CategoryTheory.StructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryStructuredArrow CategoryTheory.Comma.right	—	—
eq_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
essSurj_map₂ 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	CategoryTheory.Comma.essSurj_map CategoryTheory.Functor.instEssSurjId CategoryTheory.Discrete.instIsIsoFunctorNatTrans
eta_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
eta_inv_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Iso.inv CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—	CategoryTheory.CommaMorphism.ext CategoryTheory.Discrete.instSubsingletonDiscreteHom
ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	ext
faithful_map₂ 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	CategoryTheory.Comma.faithful_map CategoryTheory.Functor.Faithful.id
full_map₂ 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	CategoryTheory.Comma.full_map CategoryTheory.Functor.Full.id CategoryTheory.Discrete.instIsIsoFunctorNatTrans
homMk'_comp 📖	mathematical	—	homMk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma.left CategoryTheory.eqToHom	—	eqToHom_right CategoryTheory.Category.comp_id
homMk'_id 📖	mathematical	—	homMk' CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	eqToHom_right
homMk'_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map homMk' CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
homMk'_mk_comp 📖	mathematical	—	homMk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.eqToHom	—	homMk'_comp
homMk'_mk_id 📖	mathematical	—	homMk' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	homMk'_id
homMk'_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map homMk'	—	—
homMk_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Functor.map	CategoryTheory.CommaMorphism.right homMk	—	—
homMk_surjective 📖	mathematical	—	homMk	—	w
hom_eq_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	hom_ext
hom_ext 📖	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—	CategoryTheory.CommaMorphism.ext CategoryTheory.Discrete.instSubsingletonDiscreteHom
hom_ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	hom_ext
id_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.id CategoryTheory.StructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryStructuredArrow CategoryTheory.Comma.right	—	—
instEssSurjCompPre 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	CategoryTheory.Comma.instEssSurjCompPreRight
instEssSurjObjCompPostOfFull 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.StructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow post	—	CategoryTheory.Functor.map_preimage CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
instFaithfulCompPre 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	CategoryTheory.Comma.instFaithfulCompPreRight
instFaithfulObjCompPost 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.comp post	—	—
instFullCompPre 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	CategoryTheory.Comma.instFullCompPreRight
instFullObjCompPostOfFaithful 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.comp post	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Discrete.functor_map_id CategoryTheory.Category.id_comp CategoryTheory.CommaMorphism.w
isEquivalenceMap₂ 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	CategoryTheory.Comma.isEquivalenceMap CategoryTheory.Functor.isEquivalence_refl CategoryTheory.Discrete.instIsIsoFunctorNatTrans
isEquivalence_post 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.comp post	—	instFaithfulObjCompPost instFullObjCompPostOfFaithful instEssSurjObjCompPostOfFull
isEquivalence_pre 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	CategoryTheory.Comma.isEquivalence_preRight
isoMk_hom_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Iso.hom	CategoryTheory.CommaMorphism.right CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow isoMk	—	—
isoMk_inv_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Iso.hom	CategoryTheory.CommaMorphism.right CategoryTheory.Iso.inv CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow isoMk	—	—
left_eq_id 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
mapIso_counitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.inv CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapIso_counitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.inv CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapIso_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.id	—	—
mapIso_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso	—	—
mapIso_functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Iso.inv	—	—
mapIso_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso	—	—
mapIso_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso	—	—
mapIso_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.id	—	—
mapIso_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso	—	—
mapIso_inverse_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Iso.hom	—	—
mapIso_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso	—	—
mapIso_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso	—	—
mapIso_unitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.hom CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapIso_unitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapIso CategoryTheory.Functor.const CategoryTheory.Iso.hom CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapNatIso_counitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapNatIso_counitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapNatIso_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.id	—	—
mapNatIso_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso	—	—
mapNatIso_functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapNatIso_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso	—	—
mapNatIso_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso	—	—
mapNatIso_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.id	—	—
mapNatIso_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso	—	—
mapNatIso_inverse_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapNatIso_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso	—	—
mapNatIso_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso	—	—
mapNatIso_unitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapNatIso_unitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow mapNatIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
map_comp 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc
map_id 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.id_comp
map_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map CategoryTheory.CategoryStruct.id	—	—
map_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map	—	—
map_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
map_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
map_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map	—	—
map_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map	—	—
map₂_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Discrete.natTrans CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂ CategoryTheory.CategoryStruct.id	—	—
map₂_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Discrete.natTrans CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	—
map₂_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp	—	—
map₂_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	—
map₂_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow map₂	—	—
mkPostcomp_comp 📖	mathematical	—	mkPostcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.eqToHom	—	eqToHom_right CategoryTheory.Category.comp_id
mkPostcomp_id 📖	mathematical	—	mkPostcomp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	eqToHom_right
mkPostcomp_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map mkPostcomp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mkPostcomp_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map mkPostcomp	—	—
mk_hom_eq_self 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mk_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mk_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mk_surjective 📖	—	—	—	—	—
mono_homMk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map	CategoryTheory.Mono CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow homMk	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful proj_faithful
mono_of_mono_right 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful proj_faithful
obj_ext 📖	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.eqToHom	—	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
post_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.comp post homMk CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right	—	—
post_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp post CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
preEquivalenceFunctor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Functor.map preEquivalenceFunctor	—	—
preEquivalenceFunctor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre preEquivalenceFunctor CategoryTheory.CommaMorphism.right	—	—
preEquivalenceFunctor_obj_left_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre preEquivalenceFunctor	—	—
preEquivalenceFunctor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre preEquivalenceFunctor	—	—
preEquivalenceInverse_map_right_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Comma.right CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.Functor.map homMk preEquivalenceInverse	—	—
preEquivalenceInverse_obj_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.Functor.map preEquivalenceInverse	—	—
preEquivalenceInverse_obj_left_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.StructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Comma.right preEquivalenceInverse	—	—
preEquivalenceInverse_obj_right_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Comma.right CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre preEquivalenceInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	—	—
preEquivalenceInverse_obj_right_left_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Comma.right CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre preEquivalenceInverse	—	—
preEquivalenceInverse_obj_right_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre preEquivalenceInverse	—	—
preEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit preEquivalence CategoryTheory.NatIso.ofComponents preEquivalenceInverse preEquivalenceFunctor CategoryTheory.Functor.id isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.refl	—	—
preEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit preEquivalence preEquivalenceFunctor	—	—
preEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit preEquivalence preEquivalenceInverse	—	—
preEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit preEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id preEquivalenceFunctor preEquivalenceInverse isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.refl	—	—
pre_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
pre_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow pre	—	—
pre_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	—
pre_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	—
pre_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor.comp CategoryTheory.instCategoryStructuredArrow pre	—	—
prodEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryStructuredArrow prodEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp prodInverse prodFunctor CategoryTheory.Functor.id CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
prodEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryStructuredArrow prodEquivalence prodFunctor	—	—
prodEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryStructuredArrow prodEquivalence prodInverse	—	—
prodEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryStructuredArrow prodEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp prodFunctor prodInverse CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
prodFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryStructuredArrow prodFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom homMk CategoryTheory.CommaMorphism.right	—	—
prodFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.instCategoryStructuredArrow prodFunctor CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—
prodInverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.prod prodInverse homMk CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right	—	—
prodInverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.prod' CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.prod prodInverse CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom	—	—
proj_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow proj	—	ext
proj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow proj CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
proj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow proj CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
proj_reflectsIsomorphisms 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow proj	—	CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.IsIso.comp_inv_eq w CategoryTheory.CommaMorphism.ext CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsIso.inv_hom_id
toCostructuredArrow'_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.StructuredArrow CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow' CategoryTheory.CostructuredArrow.homMk Opposite.unop CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right	—	—
toCostructuredArrow'_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.StructuredArrow CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow' Opposite.unop CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—
toCostructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.StructuredArrow CategoryTheory.Category.opposite CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.Functor.op Opposite.op CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right Quiver.Hom.unop	—	—
toCostructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.StructuredArrow CategoryTheory.Category.opposite CategoryTheory.instCategoryStructuredArrow CategoryTheory.CostructuredArrow CategoryTheory.Functor.op Opposite.op CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.id_comp
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w
w_prod_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.prod' CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.prod CategoryTheory.Comma.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	—	w
w_prod_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.prod' CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.prod CategoryTheory.Comma.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w_prod_fst
w_prod_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.prod' CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.prod CategoryTheory.Comma.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	—	w
w_prod_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.prod' CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.prod CategoryTheory.Comma.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w_prod_snd

CategoryTheory.StructuredArrow.IsUniversal

Definitions

Name	Category	Theorems
desc 📖	CompOp	3 math math: hom_desc, fac_assoc, fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsUnique 📖	mathematical	—	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	fac hom_ext
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map desc	—	CategoryTheory.CommaMorphism.w CategoryTheory.Category.id_comp
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hom_desc 📖	mathematical	—	desc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	CategoryTheory.Limits.IsInitial.hom_ext
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map	—	—	hom_desc
uniq 📖	mathematical	—	CategoryTheory.Limits.IsInitial.to CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.Limits.IsInitial.hom_ext

---

← Back to Index