PullbackCone

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean

Statistics

Metric	Count
Definitions cocone, cone, ofPushoutCocone, ofPullbackCone, PullbackCone, lift', mk, eta, ext, flip, flipFlipIso, flipIsLimit, fst, isLimitAux, isLimitAux', isLimitOfFlip, isoMk, mk, mkSelfIsLimit, ofCone, snd, PushoutCocone, desc, desc', mk, eta, ext, flip, flipFlipIso, flipIsColimit, inl, inr, isColimitAux, isColimitAux', isColimitOfFlip, isoMk, mk, mkSelfIsColimit, ofCocone	39
Theorems cocone_inl, cocone_inr, cone_fst, cone_snd, ofPushoutCocone_pt, ofPushoutCocone_ι, ofPullbackCone_pt, ofPullbackCone_π, hom_ext, lift_fst, lift_fst_assoc, lift_snd, lift_snd_assoc, condition, condition_assoc, condition_one, equalizer_ext, eta_hom_hom, eta_inv_hom, flip_fst, flip_pt, flip_snd, isoMk_hom_hom, isoMk_inv_hom, mk_fst, mk_pt, mk_snd, mk_π_app, mk_π_app_left, mk_π_app_one, mk_π_app_right, ofCone_pt, ofCone_π, π_app_left, π_app_right, hom_ext, inl_desc, inl_desc_assoc, inr_desc, inr_desc_assoc, coequalizer_ext, condition, condition_assoc, condition_zero, eta_hom_hom, eta_inv_hom, flip_inl, flip_inr, flip_pt, isoMk_hom_hom, isoMk_inv_hom, mk_inl, mk_inr, mk_pt, mk_ι_app, mk_ι_app_left, mk_ι_app_right, mk_ι_app_zero, ofCocone_pt, ofCocone_ι, ι_app_left, ι_app_right	62
Total	101

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
cocone 📖	CompOp	2 math math: cocone_inl, cocone_inr
cone 📖	CompOp	2 math math: cone_snd, cone_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocone_inl 📖	mathematical	CategoryTheory.CommSq	CategoryTheory.Limits.PushoutCocone.inl cocone	—	—
cocone_inr 📖	mathematical	CategoryTheory.CommSq	CategoryTheory.Limits.PushoutCocone.inr cocone	—	—
cone_fst 📖	mathematical	CategoryTheory.CommSq	CategoryTheory.Limits.PullbackCone.fst cone	—	—
cone_snd 📖	mathematical	CategoryTheory.CommSq	CategoryTheory.Limits.PullbackCone.snd cone	—	—

CategoryTheory.Limits

Definitions

Name	Category	Theorems
PullbackCone 📖	CompOp	9 math math: pullbackConeEquivBinaryFan_functor_map_hom, pullbackConeEquivBinaryFan_counitIso, IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, pullbackConeEquivBinaryFan_inverse_obj, pullbackConeEquivBinaryFan_functor_obj, PullbackCone.eta_inv_hom, PullbackCone.eta_hom_hom, pullbackConeEquivBinaryFan_unitIso, pullbackConeEquivBinaryFan_inverse_map_hom
PushoutCocone 📖	CompOp	9 math math: pushoutCoconeEquivBinaryCofan_inverse_obj, pushoutCoconeEquivBinaryCofan_functor_obj, pushoutCoconeEquivBinaryCofan_unitIso, pushoutCoconeEquivBinaryCofan_inverse_map_hom, PushoutCocone.eta_inv_hom, pushoutCoconeEquivBinaryCofan_functor_map_hom, IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, PushoutCocone.eta_hom_hom, pushoutCoconeEquivBinaryCofan_counitIso

CategoryTheory.Limits.Cocone

Definitions

Name	Category	Theorems
ofPushoutCocone 📖	CompOp	2 math math: ofPushoutCocone_ι, ofPushoutCocone_pt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofPushoutCocone_pt 📖	mathematical	—	pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair ofPushoutCocone CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.Limits.WalkingSpan.left CategoryTheory.Limits.WalkingSpan.right CategoryTheory.Functor.map CategoryTheory.Limits.WalkingSpan.Hom.fst CategoryTheory.Limits.WalkingSpan.Hom.snd	—	—
ofPushoutCocone_ι 📖	mathematical	—	ι CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair ofPushoutCocone CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.Limits.WalkingSpan.left CategoryTheory.Limits.WalkingSpan.right CategoryTheory.Functor.map CategoryTheory.Limits.WalkingSpan.Hom.fst CategoryTheory.Limits.WalkingSpan.Hom.snd CategoryTheory.Functor.const pt CategoryTheory.Iso.hom CategoryTheory.Limits.diagramIsoSpan	—	—

CategoryTheory.Limits.Cone

Definitions

Name	Category	Theorems
ofPullbackCone 📖	CompOp	2 math math: ofPullbackCone_pt, ofPullbackCone_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofPullbackCone_pt 📖	mathematical	—	pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair ofPullbackCone CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr	—	—
ofPullbackCone_π 📖	mathematical	—	π CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair ofPullbackCone CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const pt CategoryTheory.Limits.cospan CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr CategoryTheory.Iso.inv CategoryTheory.Limits.diagramIsoCospan	—	—

CategoryTheory.Limits.PullbackCone

Definitions

Name	Category	Theorems
eta 📖	CompOp	3 math math: eta_inv_hom, eta_hom_hom, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso
ext 📖	CompOp	—
flip 📖	CompOp	3 math math: flip_fst, flip_snd, flip_pt
flipFlipIso 📖	CompOp	—
flipIsLimit 📖	CompOp	—
fst 📖	CompOp	57 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization, CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_φ, condition, TopCat.Sheaf.interUnionPullbackCone_fst, CompHausLike.pullback.isLimit_lift, unop_inl, AlgebraicGeometry.Scheme.Pullback.gluedLift_p1, IsLimit.lift_fst, CategoryTheory.IsPullback.cone_fst, IsLimit.equivPullbackObj_apply_fst, condition_assoc, combine_π_app, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, mono_fst_of_is_pullback_of_mono, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, mk_fst, isIso_fst_of_mono_of_isLimit, CategoryTheory.Limits.pullbackConeOfRightIso_fst, CategoryTheory.ChosenPullbacksAlong.pullbackCone_fst, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.pullbackConeOfLeftIso_fst, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj, π_app_left, CategoryTheory.regularTopology.parallelPair_pullback_initial, eta_inv_hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst, flip_fst, TopCat.Sheaf.interUnionPullbackConeLift_left, IsLimit.equivPullbackObj_symm_apply_fst, eta_hom_hom, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, toPullbackObj_coe_fst, flip_snd, op_inl, CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_f, CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition, CategoryTheory.regularTopology.equalizerCondition_w, CategoryTheory.mono_iff_fst_eq_snd, CategoryTheory.Limits.Types.pullbackLimitCone_isLimit, condition_one, CategoryTheory.Abelian.epi_fst_of_isLimit, fst_eq_snd_of_mono_eq, IsLimit.lift_fst_assoc, CategoryTheory.CommSq.cone_fst, CategoryTheory.mono_iff_isIso_fst, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, CategoryTheory.Limits.PushoutCocone.unop_fst, CategoryTheory.Limits.PushoutCocone.op_fst, CategoryTheory.Limits.FormalCoproduct.isPullback, fst_limit_cone, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
isLimitAux 📖	CompOp	1 math math: CategoryTheory.Limits.Types.pullbackLimitCone_isLimit
isLimitAux' 📖	CompOp	—
isLimitOfFlip 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_inv_hom, isoMk_hom_hom
mk 📖	CompOp	—
mkSelfIsLimit 📖	CompOp	—
ofCone 📖	CompOp	2 math math: ofCone_π, ofCone_pt
snd 📖	CompOp	54 math math: CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', TopCat.Sheaf.interUnionPullbackCone_snd, CategoryTheory.ChosenPullbacksAlong.pullbackCone_snd, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, π_app_right, condition, CategoryTheory.Limits.PushoutCocone.op_snd, CompHausLike.pullback.isLimit_lift, CategoryTheory.Limits.pullbackConeOfLeftIso_snd, mk_snd, condition_assoc, unop_inr, toPullbackObj_coe_snd, combine_π_app, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom, op_inr, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, AlgebraicGeometry.Scheme.Pullback.gluedLift_p2, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, snd_limit_cone, TopCat.Sheaf.interUnionPullbackConeLift_right, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj, CategoryTheory.Abelian.epi_snd_of_isLimit, IsLimit.equivPullbackObj_apply_snd, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Limits.pullbackConeOfRightIso_snd, eta_inv_hom, flip_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion, eta_hom_hom, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, flip_snd, IsLimit.lift_snd, CategoryTheory.CommSq.cone_snd, CategoryTheory.IsPullback.cone_snd, CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition, CategoryTheory.regularTopology.equalizerCondition_w, CategoryTheory.mono_iff_fst_eq_snd, CategoryTheory.Limits.Types.pullbackLimitCone_isLimit, isIso_snd_of_mono_of_isLimit, fst_eq_snd_of_mono_eq, IsLimit.lift_snd_assoc, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, CategoryTheory.mono_iff_isIso_snd, IsLimit.equivPullbackObj_symm_apply_snd, mono_snd_of_is_pullback_of_mono, CategoryTheory.Limits.PushoutCocone.unop_snd, CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft, CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_φ, CategoryTheory.Limits.FormalCoproduct.isPullback, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan fst snd	—	CategoryTheory.Limits.Cone.w
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan fst snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
condition_one 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan.one CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct fst	—	CategoryTheory.NatTrans.naturality CategoryTheory.Category.id_comp
equalizer_ext 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan fst snd	CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.Cone.w CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
eta_hom_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.pt fst snd condition CategoryTheory.Iso.hom CategoryTheory.Limits.PullbackCone CategoryTheory.Limits.Cone.category eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	condition
eta_inv_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.pt fst snd condition CategoryTheory.Iso.inv CategoryTheory.Limits.PullbackCone CategoryTheory.Limits.Cone.category eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	condition
flip_fst 📖	mathematical	—	fst flip snd	—	—
flip_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan flip	—	—
flip_snd 📖	mathematical	—	snd flip fst	—	—
isoMk_hom_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.diagramIsoCospan CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.naturality isoMk CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.naturality
isoMk_inv_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cones.postcompose CategoryTheory.Iso.hom CategoryTheory.Limits.diagramIsoCospan CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.naturality isoMk CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.naturality
mk_fst 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	fst	—	—
mk_pt 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	—
mk_snd 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	snd	—	—
mk_π_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π	—	—
mk_π_app_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan.left	—	—
mk_π_app_one 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan.one	—	—
mk_π_app_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan.right	—	—
ofCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr ofCone	—	—
ofCone_π 📖	mathematical	—	CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr ofCone CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.hom CategoryTheory.Limits.diagramIsoCospan	—	—
π_app_left 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan.left fst	—	—
π_app_right 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.cospan CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingCospan.right snd	—	—

CategoryTheory.Limits.PullbackCone.IsLimit

Definitions

Name	Category	Theorems
lift' 📖	CompOp	—
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PullbackCone.fst CategoryTheory.Limits.PullbackCone.snd	—	—	CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.PullbackCone.equalizer_ext
lift_fst 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan lift CategoryTheory.Limits.PullbackCone.fst	—	CategoryTheory.Limits.IsLimit.fac
lift_fst_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan lift CategoryTheory.Limits.PullbackCone.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fst
lift_snd 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan lift CategoryTheory.Limits.PullbackCone.snd	—	CategoryTheory.Limits.IsLimit.fac
lift_snd_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan lift CategoryTheory.Limits.PullbackCone.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_snd

CategoryTheory.Limits.PushoutCocone

Definitions

Name	Category	Theorems
eta 📖	CompOp	3 math math: CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, eta_inv_hom, eta_hom_hom
ext 📖	CompOp	—
flip 📖	CompOp	3 math math: flip_pt, flip_inr, flip_inl
flipFlipIso 📖	CompOp	—
flipIsColimit 📖	CompOp	—
inl 📖	CompOp	37 math math: inl_colimit_cocone, flip_inr, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit, inl_eq_inr_of_epi_eq, condition_assoc, CategoryTheory.Limits.PullbackCone.unop_inl, CommRingCat.pushoutCocone_inl, epi_inl_of_is_pushout_of_epi, CategoryTheory.IsPushout.cocone_inl, condition, CategoryTheory.CommSq.cocone_inl, CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl, CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso, eta_inv_hom, condition_zero, ι_app_left, isIso_inl_of_epi_of_isColimit, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom, IsColimit.inl_desc_assoc, CategoryTheory.epi_iff_inl_eq_inr, mk_inl, CategoryTheory.Limits.PullbackCone.op_inl, CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, IsColimit.inl_desc, CategoryTheory.Abelian.mono_inl_of_isColimit, flip_inl, CategoryTheory.epi_iff_isIso_inl, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inl, eta_hom_hom, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.Limits.pushoutCoconeOfRightIso_inl, unop_fst, op_fst
inr 📖	CompOp	36 math math: flip_inr, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, mk_inr, CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit, inl_eq_inr_of_epi_eq, condition_assoc, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inr, op_snd, CategoryTheory.IsPushout.cocone_inr, condition, CategoryTheory.Limits.PullbackCone.unop_inr, CommRingCat.pushoutCocone_inr, CategoryTheory.Limits.PullbackCone.op_inr, CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso, CategoryTheory.CommSq.cocone_inr, eta_inv_hom, ι_app_right, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom, inr_colimit_cocone, CategoryTheory.epi_iff_inl_eq_inr, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, IsColimit.inr_desc_assoc, IsColimit.inr_desc, epi_inr_of_is_pushout_of_epi, flip_inl, eta_hom_hom, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.Abelian.mono_inr_of_isColimit, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.Limits.pushoutCoconeOfRightIso_inr, isIso_inr_of_epi_of_isColimit, unop_snd, CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr, CategoryTheory.epi_iff_isIso_inr, CategoryTheory.Limits.Types.pushoutCocone_inr_injective_of_isColimit
isColimitAux 📖	CompOp	—
isColimitAux' 📖	CompOp	—
isColimitOfFlip 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_inv_hom, isoMk_hom_hom
mk 📖	CompOp	—
mkSelfIsColimit 📖	CompOp	—
ofCocone 📖	CompOp	2 math math: ofCocone_ι, ofCocone_pt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coequalizer_ext 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inl inr	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Limits.Cocone.w CategoryTheory.Category.assoc
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inl inr	—	CategoryTheory.Limits.Cocone.w
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inl inr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
condition_zero 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inl	—	CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id
eta_hom_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.Cocone.pt inl inr condition CategoryTheory.Iso.hom CategoryTheory.Limits.PushoutCocone CategoryTheory.Limits.Cocone.category eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	condition
eta_inv_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.Cocone.pt inl inr condition CategoryTheory.Iso.inv CategoryTheory.Limits.PushoutCocone CategoryTheory.Limits.Cocone.category eta CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	condition
flip_inl 📖	mathematical	—	inl flip inr	—	—
flip_inr 📖	mathematical	—	inr flip inl	—	—
flip_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span flip	—	—
isoMk_hom_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.Limits.WalkingSpan.left CategoryTheory.Limits.WalkingSpan.right CategoryTheory.Functor.map CategoryTheory.Limits.WalkingSpan.Hom.fst CategoryTheory.Limits.WalkingSpan.Hom.snd CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.diagramIsoSpan CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.naturality isoMk CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.naturality
isoMk_inv_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.Limits.WalkingSpan.left CategoryTheory.Limits.WalkingSpan.right CategoryTheory.Functor.map CategoryTheory.Limits.WalkingSpan.Hom.fst CategoryTheory.Limits.WalkingSpan.Hom.snd CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Iso.inv CategoryTheory.Limits.diagramIsoSpan Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.naturality isoMk CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.naturality
mk_inl 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	inl	—	—
mk_inr 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	inr	—	—
mk_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span	—	—
mk_ι_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	—
mk_ι_app_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan.left	—	—
mk_ι_app_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan.right	—	—
mk_ι_app_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan.zero	—	—
ofCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.Limits.WalkingSpan.left CategoryTheory.Limits.WalkingSpan.right CategoryTheory.Functor.map CategoryTheory.Limits.WalkingSpan.Hom.fst CategoryTheory.Limits.WalkingSpan.Hom.snd ofCocone	—	—
ofCocone_ι 📖	mathematical	—	CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingSpan.zero CategoryTheory.Limits.WalkingSpan.left CategoryTheory.Limits.WalkingSpan.right CategoryTheory.Functor.map CategoryTheory.Limits.WalkingSpan.Hom.fst CategoryTheory.Limits.WalkingSpan.Hom.snd ofCocone CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Iso.inv CategoryTheory.Limits.diagramIsoSpan	—	—
ι_app_left 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan.left inl	—	—
ι_app_right 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingSpan.right inr	—	—

CategoryTheory.Limits.PushoutCocone.IsColimit

Definitions

Name	Category	Theorems
desc 📖	CompOp	4 math math: inl_desc_assoc, inr_desc_assoc, inr_desc, inl_desc
desc' 📖	CompOp	—
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inl CategoryTheory.Limits.PushoutCocone.inr	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.PushoutCocone.coequalizer_ext
inl_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inl desc	—	CategoryTheory.Limits.IsColimit.fac
inl_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inl desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_desc
inr_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inr desc	—	CategoryTheory.Limits.IsColimit.fac
inr_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inr desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_desc

---

← Back to Index