Cone

📁 Source: Mathlib/CategoryTheory/WithTerminal/Cone.lean

Statistics

Metric	Count
Definitions Cone, coconeEquiv, commaFromUnder, isColimitEquiv, liftFromUnder, liftFromUnderComp, commaFromOver, coneEquiv, isLimitEquiv, liftFromOver, liftFromOverComp	11
Theorems hasLimit_of_hasLimit_liftFromOver, coconeEquiv_counitIso_hom_app_hom, coconeEquiv_counitIso_inv_app_hom, coconeEquiv_functor_map_hom, coconeEquiv_functor_obj_pt, coconeEquiv_functor_obj_ι_app_of, coconeEquiv_functor_obj_ι_app_star, coconeEquiv_inverse_map_hom_right, coconeEquiv_inverse_obj_pt_hom, coconeEquiv_inverse_obj_pt_left_as, coconeEquiv_inverse_obj_pt_right, coconeEquiv_inverse_obj_ι_app_right, coconeEquiv_unitIso_hom_app_hom_right, coconeEquiv_unitIso_inv_app_hom_right, commaFromUnder_map_left, commaFromUnder_map_right, commaFromUnder_obj_hom_app, commaFromUnder_obj_left, commaFromUnder_obj_right, isColimitEquiv_apply_desc_right, isColimitEquiv_symm_apply_desc, liftFromUnderComp_hom_app, liftFromUnderComp_inv_app, liftFromUnder_map_app, liftFromUnder_obj_map, liftFromUnder_obj_obj, commaFromOver_map_left, commaFromOver_map_right, commaFromOver_obj_hom_app, commaFromOver_obj_left, commaFromOver_obj_right, coneEquiv_counitIso_hom_app_hom, coneEquiv_counitIso_inv_app_hom, coneEquiv_functor_map_hom, coneEquiv_functor_obj_pt, coneEquiv_functor_obj_π_app_of, coneEquiv_functor_obj_π_app_star, coneEquiv_inverse_map_hom_left, coneEquiv_inverse_obj_pt_hom, coneEquiv_inverse_obj_pt_left, coneEquiv_inverse_obj_pt_right_as, coneEquiv_inverse_obj_π_app_left, coneEquiv_unitIso_hom_app_hom_left, coneEquiv_unitIso_inv_app_hom_left, isLimitEquiv_apply_lift_left, isLimitEquiv_symm_apply_lift, liftFromOverComp_hom_app, liftFromOverComp_inv_app, liftFromOver_map_app, liftFromOver_obj_map, liftFromOver_obj_obj, instHasLimitsOfShapeOverOfWithTerminal, instHasLimitsOfSizeOver, hasColimit_of_hasColimit_liftFromUnder, instHasColimitsOfShapeUnderOfWithInitial, instHasColimitsOfSizeUnder	56
Total	67

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLimitsOfShapeOverOfWithTerminal 📖	mathematical	—	Limits.HasLimitsOfShape Over instCategoryOver	—	Over.hasLimit_of_hasLimit_liftFromOver Limits.hasLimitOfHasLimitsOfShape
instHasLimitsOfSizeOver 📖	mathematical	—	Limits.HasLimitsOfSize Over instCategoryOver	—	instHasLimitsOfShapeOverOfWithTerminal Limits.hasLimitsOfShapeOfHasLimits

CategoryTheory.Limits

Definitions

Name	Category	Theorems
Cone 📖	CompData	240 math math: DiagramOfCones.id, CategoryTheory.Functor.Initial.extendCone_obj_pt, CategoryTheory.WithTerminal.coneEquiv_unitIso_hom_app_hom_left, IsLimit.ofConeEquiv_symm_apply_desc, Cone.reflects_cone_isomorphism, ConeMorphism.hom_inv_id, hasLimit_iff_hasTerminal_cone, CategoryTheory.Functor.mapConeMapCone_hom_hom, coneOpEquiv_unitIso, Cone.postcomposeComp_hom_app_hom, coconeLeftOpOfConeEquiv_functor_map_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, coneRightOpOfCoconeEquiv_functor_obj, CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom, IsLimit.liftConeMorphism_eq_isTerminal_from, ConeMorphism.inv_hom_id_assoc, Cone.functoriality_full, coneRightOpOfCoconeEquiv_functor_map_hom, coneUnopOfCoconeEquiv_counitIso, HasLimit.lift_isoOfNatIso_hom, Cone.equiv_inv_pt, CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom, Cone.postcomposeEquivalence_functor, Cone.whiskeringEquivalence_functor, Cone.functorialityEquivalence_inverse, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_π_app_left, Cone.postcomposeComp_inv_app_hom, Cone.ext_inv_inv_hom, Cone.eta_hom_hom, Cone.fromCostructuredArrow_map_hom, Cone.toCostructuredArrow_obj, CategoryTheory.Functor.mapConePostcompose_inv_hom, Cone.extendIso_hom_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, coconeUnopOfConeEquiv_unitIso, Cone.extendId_hom_hom, IsLimit.uniqueUpToIso_inv, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_inv_app_hom_left, CategoryTheory.Over.conePost_obj_π_app, Cone.cone_iso_of_hom_iso, CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso, Cone.forget_obj, CategoryTheory.Functor.functorialityCompPostcompose_hom_app_hom, Cone.fromCostructuredArrow_obj_π, Cone.postcomposeEquivalence_unitIso, coconeLeftOpOfConeEquiv_inverse_obj, CategoryTheory.Functor.Initial.conesEquiv_counitIso, Cone.postcompose_obj_pt, Fork.ι_postcompose, CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_star, CategoryTheory.WithTerminal.coneEquiv_counitIso_inv_app_hom, coconeRightOpOfConeEquiv_functor_map_hom, CategoryTheory.Functor.mapCoconeOp_inv_hom, coneRightOpOfCoconeEquiv_inverse_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, Cone.equivCostructuredArrow_inverse, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, IsLimit.ofIsoLimit_lift, CategoryTheory.Functor.Initial.extendCone_obj_π_app', coneOpEquiv_inverse_obj, Cone.functorialityEquivalence_counitIso, coconeUnopOfConeEquiv_counitIso, coconeUnopOfConeEquiv_functor_obj, CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_of, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, CategoryTheory.Over.conePostIso_hom_app_hom, CategoryTheory.Functor.RightExtension.coneAtFunctor_obj, coconeUnopOfConeEquiv_functor_map_hom, Cone.category_id_hom, coconeOpEquiv_inverse_map, IsLimit.equivIsoLimit_symm_apply, DiagramOfCones.mkOfHasLimits_map_hom, coconeOpEquiv_functor_obj, Cone.whiskeringEquivalence_unitIso, Cone.postcompose_obj_π, Cone.equiv_hom_fst, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, IsLimit.ofConeEquiv_apply_desc, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom, coconeUnopOfConeEquiv_inverse_map, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_left, Cone.whiskering_map_hom, IsLimit.uniqueUpToIso_hom, CategoryTheory.Over.conePost_map_hom, CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_inv_hom, Cone.postcomposeEquivalence_counitIso, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_inv_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, CategoryTheory.Functor.Initial.conesEquiv_unitIso, coneLeftOpOfCoconeEquiv_inverse_obj, DiagramOfCones.conePoints_map, Cone.mapConeToUnder_inv_hom, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_inv_app_hom, Cones.functoriality_faithful, coconeRightOpOfConeEquiv_inverse_obj, Cone.extendId_inv_hom, coneOpEquiv_functor_obj, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom, coconeRightOpOfConeEquiv_unitIso, CategoryTheory.Over.ConstructProducts.conesEquivCounitIso_hom_app_hom_left, coneOpEquiv_counitIso, coneUnopOfCoconeEquiv_functor_map_hom, CategoryTheory.IsCofiltered.iff_cone_nonempty, Cone.extendComp_inv_hom, CategoryTheory.Functor.Initial.extendCone_map_hom, Cone.toCostructuredArrow_map, CategoryTheory.Functor.Initial.conesEquiv_inverse, CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso, Cone.equiv_inv_π, instIsIsoHomInvCone, CategoryTheory.IsCofiltered.cone_nonempty, coconeRightOpOfConeEquiv_inverse_map, Cone.equiv_hom_snd, Cone.functoriality_obj_π_app, PullbackCone.unop_ι_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, PullbackCone.isoMk_inv_hom, coneRightOpOfCoconeEquiv_inverse_map, Cones.functoriality_full, CategoryTheory.Adjunction.functorialityUnit'_app_hom, coneUnopOfCoconeEquiv_functor_obj, colimitLimitToLimitColimitCone_iso, CategoryTheory.liftedLimitMapsToOriginal_inv_map_π, coneUnopOfCoconeEquiv_inverse_obj, Cone.equivalenceOfReindexing_functor, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom, Cone.equivCostructuredArrow_functor, Cone.whiskeringEquivalence_counitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, CategoryTheory.Over.conePostIso_inv_app_hom, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, Cone.functoriality_obj_pt, pointwiseBinaryBicone.isBilimit_isLimit, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, coconeLeftOpOfConeEquiv_unitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, Cone.ext_inv_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, CategoryTheory.Over.conePost_obj_pt, coconeOpEquiv_inverse_obj, CategoryTheory.Over.ConstructProducts.conesEquiv_functor, CategoryTheory.Functor.mapConeWhisker_hom_hom, Cone.equivCostructuredArrow_counitIso, coneOpEquiv_functor_map_hom, Cone.ext_inv_hom_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, Cone.category_comp_hom, coconeOpEquiv_unitIso, CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom, ConeMorphism.hom_inv_id_assoc, Cone.ext_hom_hom, Cone.functorialityEquivalence_functor, Cone.fromCostructuredArrow_obj_pt, coneLeftOpOfCoconeEquiv_functor_map_hom, coneLeftOpOfCoconeEquiv_functor_obj, coneLeftOpOfCoconeEquiv_unitIso, coneLeftOpOfCoconeEquiv_inverse_map, coconeRightOpOfConeEquiv_counitIso, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, limit.lift_map, coconeRightOpOfConeEquiv_functor_obj, IsLimit.conePointsIsoOfEquivalence_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, CategoryTheory.Functor.RightExtension.coneAtFunctor_map_hom, Cone.whiskering_obj, CategoryTheory.Functor.mapConePostcompose_hom_hom, IsLimit.conePointsIsoOfEquivalence_inv, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_pt, CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_hom_hom, coneOpEquiv_inverse_map, CategoryTheory.WithTerminal.coneEquiv_unitIso_inv_app_hom_left, coconeUnopOfConeEquiv_inverse_obj, DiagramOfCones.comp, CategoryTheory.Functor.mapCoconeOp_hom_hom, Cone.equivalenceOfReindexing_counitIso, CategoryTheory.Over.ConstructProducts.conesEquivUnitIso_hom_app_hom, coneLeftOpOfCoconeEquiv_counitIso, Cone.equivalenceOfReindexing_unitIso, Cone.mapConeToUnder_hom_hom, Cone.functoriality_map_hom, CategoryTheory.Over.ConstructProducts.conesEquivInverse_obj, Cone.postcomposeId_inv_app_hom, coneUnopOfCoconeEquiv_inverse_map, CategoryTheory.Functor.Initial.limitConeOfComp_cone, Cone.equivCostructuredArrow_unitIso, Cone.instIsIsoExtendHom, Cone.equivalenceOfReindexing_inverse, coconeOpEquiv_counitIso, Cone.extendComp_hom_hom, coconeLeftOpOfConeEquiv_counitIso, CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left, CategoryTheory.Functor.mapConeMapCone_inv_hom, PullbackCone.isoMk_hom_hom, CategoryTheory.Functor.Initial.extendCone_obj_π_app, Cone.extendIso_inv_hom, CategoryTheory.Functor.functorialityCompPostcompose_inv_app_hom, Cone.postcomposeId_hom_app_hom, CategoryTheory.Functor.mapConeWhisker_inv_hom, Cone.forget_map, CategoryTheory.WithTerminal.coneEquiv_functor_obj_pt, coneRightOpOfCoconeEquiv_unitIso, CategoryTheory.Over.ConstructProducts.conesEquiv_inverse, CategoryTheory.liftedLimitMapsToOriginal_hom_π, Cone.whiskeringEquivalence_inverse, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, HasLimit.lift_isoOfNatIso_inv, limit.lift_map_assoc, Cones.reflects_cone_isomorphism, CategoryTheory.Functor.Initial.conesEquiv_functor, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, Cone.postcomposeEquivalence_inverse, Cones.cone_iso_of_hom_iso, Cone.postcompose_map_hom, Cone.eta_inv_hom, HasLimit.lift_isoOfNatIso_hom_assoc, coconeLeftOpOfConeEquiv_inverse_map, Cone.functoriality_faithful, coconeOpEquiv_functor_map_hom, IsTerminal.from_eq_liftConeMorphism, FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone, coneUnopOfCoconeEquiv_unitIso, CategoryTheory.WithTerminal.coneEquiv_counitIso_hom_app_hom, coconeLeftOpOfConeEquiv_functor_obj, CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app, IsLimit.hom_isIso, CategoryTheory.Functor.Initial.limitConeOfComp_isLimit, instIsIsoHomHomCone, CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom, CategoryTheory.Adjunction.functorialityCounit'_app_hom, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as, coneRightOpOfCoconeEquiv_counitIso, HasLimit.lift_isoOfNatIso_inv_assoc, ConeMorphism.inv_hom_id, CategoryTheory.WithTerminal.coneEquiv_functor_map_hom, Cone.functorialityEquivalence_unitIso

CategoryTheory.Over

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimit_of_hasLimit_liftFromOver 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Over CategoryTheory.instCategoryOver	—	—

CategoryTheory.WithInitial

Definitions

Name	Category	Theorems
coconeEquiv 📖	CompOp	15 math math: isColimitEquiv_apply_desc_right, coconeEquiv_functor_obj_pt, coconeEquiv_inverse_obj_pt_right, isColimitEquiv_symm_apply_desc, coconeEquiv_inverse_obj_pt_hom, coconeEquiv_counitIso_inv_app_hom, coconeEquiv_functor_obj_ι_app_star, coconeEquiv_unitIso_hom_app_hom_right, coconeEquiv_functor_map_hom, coconeEquiv_inverse_obj_pt_left_as, coconeEquiv_inverse_obj_ι_app_right, coconeEquiv_functor_obj_ι_app_of, coconeEquiv_inverse_map_hom_right, coconeEquiv_counitIso_hom_app_hom, coconeEquiv_unitIso_inv_app_hom_right
commaFromUnder 📖	CompOp	6 math math: commaFromUnder_map_left, commaFromUnder_obj_hom_app, commaFromUnder_obj_right, commaFromUnder_map_right, commaFromUnder_obj_left, liftFromUnder_map_app
isColimitEquiv 📖	CompOp	2 math math: isColimitEquiv_apply_desc_right, isColimitEquiv_symm_apply_desc
liftFromUnder 📖	CompOp	20 math math: isColimitEquiv_apply_desc_right, coconeEquiv_functor_obj_pt, coconeEquiv_inverse_obj_pt_right, isColimitEquiv_symm_apply_desc, liftFromUnderComp_inv_app, coconeEquiv_inverse_obj_pt_hom, coconeEquiv_counitIso_inv_app_hom, coconeEquiv_functor_obj_ι_app_star, coconeEquiv_unitIso_hom_app_hom_right, liftFromUnder_obj_obj, coconeEquiv_functor_map_hom, coconeEquiv_inverse_obj_pt_left_as, coconeEquiv_inverse_obj_ι_app_right, coconeEquiv_functor_obj_ι_app_of, coconeEquiv_inverse_map_hom_right, liftFromUnderComp_hom_app, coconeEquiv_counitIso_hom_app_hom, liftFromUnder_map_app, liftFromUnder_obj_map, coconeEquiv_unitIso_inv_app_hom_right
liftFromUnderComp 📖	CompOp	2 math math: liftFromUnderComp_inv_app, liftFromUnderComp_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeEquiv_counitIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso coconeEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt	—	—
coconeEquiv_counitIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso coconeEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt	—	—
coconeEquiv_functor_map_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.const Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor coconeEquiv	—	—
coconeEquiv_functor_obj_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor coconeEquiv CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—
coconeEquiv_functor_obj_ι_app_of 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor coconeEquiv CategoryTheory.Limits.Cocone.ι of CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—
coconeEquiv_functor_obj_ι_app_star 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor coconeEquiv CategoryTheory.Limits.Cocone.ι star CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—
coconeEquiv_inverse_map_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const liftFromUnder star CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left of CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.map CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.inverse coconeEquiv	—	—
coconeEquiv_inverse_obj_pt_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.WithInitial instCategory CategoryTheory.Functor CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.inverse coconeEquiv CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι star	—	—
coconeEquiv_inverse_obj_pt_left_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.WithInitial instCategory CategoryTheory.Functor CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.inverse coconeEquiv	—	—
coconeEquiv_inverse_obj_pt_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.WithInitial instCategory CategoryTheory.Functor CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.inverse coconeEquiv	—	—
coconeEquiv_inverse_obj_ι_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.WithInitial instCategory CategoryTheory.Limits.Cocone.pt liftFromUnder star CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.inverse coconeEquiv of	—	—
coconeEquiv_unitIso_hom_app_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.WithInitial instCategory liftFromUnder coconeEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
coconeEquiv_unitIso_inv_app_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.WithInitial instCategory liftFromUnder coconeEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
commaFromUnder_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.forget CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory commaFromUnder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
commaFromUnder_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.forget CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory commaFromUnder CategoryTheory.Functor.whiskerRight	—	—
commaFromUnder_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.forget CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory commaFromUnder CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
commaFromUnder_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Comma CategoryTheory.commaCategory commaFromUnder	—	—
commaFromUnder_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Comma CategoryTheory.commaCategory commaFromUnder CategoryTheory.Functor.comp CategoryTheory.Under.forget	—	—
isColimitEquiv_apply_desc_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Limits.IsColimit.desc DFunLike.coe Equiv CategoryTheory.Limits.IsColimit CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor coconeEquiv EquivLike.toFunLike Equiv.instEquivLike isColimitEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Limits.IsColimit.ofLeftAdjoint CategoryTheory.Equivalence.toAdjunction CategoryTheory.Equivalence.symm	—	CategoryTheory.Category.id_comp
isColimitEquiv_symm_apply_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Equivalence.functor coconeEquiv DFunLike.coe Equiv CategoryTheory.Limits.IsColimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm isColimitEquiv CategoryTheory.Limits.CoconeMorphism.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Equivalence.inverse CategoryTheory.Adjunction.homEquiv CategoryTheory.Equivalence.toAdjunction CategoryTheory.Limits.IsColimit.descCoconeMorphism	—	—
liftFromUnderComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Functor.comp CategoryTheory.Under.post CategoryTheory.Iso.hom liftFromUnderComp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id star of	—	—
liftFromUnderComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Under.post CategoryTheory.Iso.inv liftFromUnderComp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id star of	—	—
liftFromUnder_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma CategoryTheory.Under CategoryTheory.instCategoryUnder commaFromUnder CategoryTheory.Functor.map liftFromUnder Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.right CategoryTheory.CategoryStruct.id	—	—
liftFromUnder_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right down CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
liftFromUnder_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory CategoryTheory.Functor CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.category liftFromUnder CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—

CategoryTheory.WithTerminal

Definitions

Name	Category	Theorems
commaFromOver 📖	CompOp	6 math math: commaFromOver_map_left, commaFromOver_obj_right, commaFromOver_obj_hom_app, commaFromOver_map_right, liftFromOver_map_app, commaFromOver_obj_left
coneEquiv 📖	CompOp	15 math math: coneEquiv_unitIso_hom_app_hom_left, coneEquiv_inverse_obj_π_app_left, coneEquiv_functor_obj_π_app_star, coneEquiv_counitIso_inv_app_hom, coneEquiv_functor_obj_π_app_of, coneEquiv_inverse_obj_pt_left, isLimitEquiv_symm_apply_lift, coneEquiv_inverse_obj_pt_hom, isLimitEquiv_apply_lift_left, coneEquiv_unitIso_inv_app_hom_left, coneEquiv_inverse_map_hom_left, coneEquiv_functor_obj_pt, coneEquiv_counitIso_hom_app_hom, coneEquiv_inverse_obj_pt_right_as, coneEquiv_functor_map_hom
isLimitEquiv 📖	CompOp	2 math math: isLimitEquiv_symm_apply_lift, isLimitEquiv_apply_lift_left
liftFromOver 📖	CompOp	20 math math: coneEquiv_unitIso_hom_app_hom_left, coneEquiv_inverse_obj_π_app_left, coneEquiv_functor_obj_π_app_star, coneEquiv_counitIso_inv_app_hom, coneEquiv_functor_obj_π_app_of, coneEquiv_inverse_obj_pt_left, isLimitEquiv_symm_apply_lift, liftFromOver_obj_obj, coneEquiv_inverse_obj_pt_hom, liftFromOverComp_hom_app, liftFromOver_obj_map, isLimitEquiv_apply_lift_left, coneEquiv_unitIso_inv_app_hom_left, liftFromOverComp_inv_app, liftFromOver_map_app, coneEquiv_inverse_map_hom_left, coneEquiv_functor_obj_pt, coneEquiv_counitIso_hom_app_hom, coneEquiv_inverse_obj_pt_right_as, coneEquiv_functor_map_hom
liftFromOverComp 📖	CompOp	2 math math: liftFromOverComp_hom_app, liftFromOverComp_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commaFromOver_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory commaFromOver CategoryTheory.Functor.whiskerRight	—	—
commaFromOver_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget CategoryTheory.Functor.obj CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory commaFromOver CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
commaFromOver_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory commaFromOver CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
commaFromOver_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma CategoryTheory.commaCategory commaFromOver CategoryTheory.Functor.comp CategoryTheory.Over.forget	—	—
commaFromOver_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma CategoryTheory.commaCategory commaFromOver	—	—
coneEquiv_counitIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso coneEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquiv_counitIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso coneEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
coneEquiv_functor_map_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.const Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.left CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor coneEquiv	—	—
coneEquiv_functor_obj_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor coneEquiv CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
coneEquiv_functor_obj_π_app_of 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor coneEquiv CategoryTheory.Limits.Cone.π of CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
coneEquiv_functor_obj_π_app_star 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor coneEquiv CategoryTheory.Limits.Cone.π star CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
coneEquiv_inverse_map_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const liftFromOver star CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π of CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.map CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.inverse coneEquiv	—	—
coneEquiv_inverse_obj_pt_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.WithTerminal instCategory CategoryTheory.Functor CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.inverse coneEquiv CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π star	—	—
coneEquiv_inverse_obj_pt_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.WithTerminal instCategory CategoryTheory.Functor CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.inverse coneEquiv	—	—
coneEquiv_inverse_obj_pt_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.WithTerminal instCategory CategoryTheory.Functor CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.inverse coneEquiv	—	—
coneEquiv_inverse_obj_π_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.WithTerminal instCategory CategoryTheory.Limits.Cone.pt liftFromOver star CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.inverse coneEquiv of	—	—
coneEquiv_unitIso_hom_app_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.WithTerminal instCategory liftFromOver coneEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
coneEquiv_unitIso_inv_app_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.WithTerminal instCategory liftFromOver coneEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
isLimitEquiv_apply_lift_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Limits.IsLimit.lift DFunLike.coe Equiv CategoryTheory.Limits.IsLimit CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor coneEquiv EquivLike.toFunLike Equiv.instEquivLike isLimitEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Limits.IsLimit.ofRightAdjoint CategoryTheory.Equivalence.toAdjunction	—	CategoryTheory.Category.comp_id
isLimitEquiv_symm_apply_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm coneEquiv DFunLike.coe Equiv CategoryTheory.Limits.IsLimit CategoryTheory.Equivalence.functor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm isLimitEquiv CategoryTheory.Limits.ConeMorphism.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Adjunction.homEquiv CategoryTheory.Equivalence.toAdjunction CategoryTheory.Limits.IsLimit.liftConeMorphism	—	—
liftFromOverComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Functor.comp CategoryTheory.Over.post CategoryTheory.Iso.hom liftFromOverComp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id star of	—	—
liftFromOverComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Over.post CategoryTheory.Iso.inv liftFromOverComp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id star of	—	—
liftFromOver_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma CategoryTheory.Over CategoryTheory.instCategoryOver commaFromOver CategoryTheory.Functor.map liftFromOver Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left CategoryTheory.CategoryStruct.id	—	—
liftFromOver_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left down CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
liftFromOver_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory CategoryTheory.Functor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.category liftFromOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—

Under

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit_of_hasColimit_liftFromUnder 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Under CategoryTheory.instCategoryUnder	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimitsOfShapeUnderOfWithInitial 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Under CategoryTheory.instCategoryUnder	—	Under.hasColimit_of_hasColimit_liftFromUnder CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instHasColimitsOfSizeUnder 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize CategoryTheory.Under CategoryTheory.instCategoryUnder	—	instHasColimitsOfShapeUnderOfWithInitial CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize

---

← Back to Index