Pullbacks

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean

Statistics

Metric	Count
Definitions coconeOp, coconeUnop, coneOp, coneUnop, isLimitEquivIsColimitOp, isLimitEquivIsColimitUnop, op, opUnopIso, unop, unopOpIso, isColimitEquivIsLimitOp, isColimitEquivIsLimitUnop, op, opUnopIso, unop, unopOpIso, cospanOp, cospanUnop, opCospan, opSpan, pullbackIsoOpPushout, pullbackIsoUnopPushout, pushoutIsoOpPullback, pushoutIsoUnopPullback, spanOp, spanUnop	26
Theorems op_inl, op_inr, op_pt, op_ι_app, unop_inl, unop_inr, unop_pt, unop_ι_app, op_fst, op_pt, op_snd, op_π_app, unop_fst, unop_pt, unop_snd, unop_π_app, cospanOp_hom_app, cospanOp_inv_app, cospanUnop_hom_app, cospanUnop_inv_app, hasPullback_op_iff_hasPushout, hasPullback_unop_iff_hasPushout, hasPullbacks_opposite, hasPushout_op_iff_hasPullback, hasPushout_unop_iff_hasPullback, hasPushouts_opposite, instHasPullbackOppositeOpOfHasPushout, instHasPullbackUnopOfHasPushoutOpposite, instHasPushoutOppositeOpOfHasPullback, instHasPushoutUnopOfHasPullbackOpposite, opCospan_hom_app, opCospan_inv_app, opSpan_hom_app, opSpan_inv_app, op_pullbackMap, op_pushoutMap, pullbackIsoOpPushout_hom_inl, pullbackIsoOpPushout_hom_inl_assoc, pullbackIsoOpPushout_hom_inr, pullbackIsoOpPushout_hom_inr_assoc, pullbackIsoOpPushout_inv_fst, pullbackIsoOpPushout_inv_fst_assoc, pullbackIsoOpPushout_inv_snd, pullbackIsoOpPushout_inv_snd_assoc, pullbackIsoUnopPushout_hom_inl, pullbackIsoUnopPushout_hom_inl_assoc, pullbackIsoUnopPushout_hom_inr, pullbackIsoUnopPushout_hom_inr_assoc, pullbackIsoUnopPushout_inv_fst, pullbackIsoUnopPushout_inv_fst_assoc, pullbackIsoUnopPushout_inv_snd, pullbackIsoUnopPushout_inv_snd_assoc, pushoutIsoOpPullback_inl_hom, pushoutIsoOpPullback_inl_hom_assoc, pushoutIsoOpPullback_inr_hom, pushoutIsoOpPullback_inr_hom_assoc, pushoutIsoOpPullback_inv_fst, pushoutIsoOpPullback_inv_snd, pushoutIsoUnopPullback_inl_hom, pushoutIsoUnopPullback_inl_hom_assoc, pushoutIsoUnopPullback_inr_hom, pushoutIsoUnopPullback_inr_hom_assoc, pushoutIsoUnopPullback_inv_fst, pushoutIsoUnopPullback_inv_snd, spanOp_hom_app, spanOp_inv_app, spanUnop_hom_app, spanUnop_inv_app	68
Total	94

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
coconeOp 📖	CompOp	—
coconeUnop 📖	CompOp	—
coneOp 📖	CompOp	—
coneUnop 📖	CompOp	—

CategoryTheory.Limits

Definitions

Name	Category	Theorems
cospanOp 📖	CompOp	2 math math: cospanOp_hom_app, cospanOp_inv_app
cospanUnop 📖	CompOp	2 math math: cospanUnop_hom_app, cospanUnop_inv_app
opCospan 📖	CompOp	3 math math: PushoutCocone.unop_π_app, opCospan_hom_app, opCospan_inv_app
opSpan 📖	CompOp	3 math math: opSpan_hom_app, PullbackCone.unop_ι_app, opSpan_inv_app
pullbackIsoOpPushout 📖	CompOp	10 math math: pullbackIsoOpPushout_hom_inr_assoc, op_pushoutMap, pullbackIsoOpPushout_inv_fst_assoc, pullbackIsoOpPushout_inv_fst, pullbackIsoOpPushout_inv_snd, pullbackIsoOpPushout_hom_inl, pushout.op_codiagonal, pullbackIsoOpPushout_hom_inr, pullbackIsoOpPushout_inv_snd_assoc, pullbackIsoOpPushout_hom_inl_assoc
pullbackIsoUnopPushout 📖	CompOp	8 math math: pullbackIsoUnopPushout_inv_snd, pullbackIsoUnopPushout_hom_inr_assoc, pullbackIsoUnopPushout_hom_inl, pullbackIsoUnopPushout_inv_fst, pullbackIsoUnopPushout_hom_inl_assoc, pullbackIsoUnopPushout_inv_fst_assoc, pullbackIsoUnopPushout_inv_snd_assoc, pullbackIsoUnopPushout_hom_inr
pushoutIsoOpPullback 📖	CompOp	7 math math: pushoutIsoOpPullback_inr_hom_assoc, pushoutIsoOpPullback_inl_hom, pushoutIsoOpPullback_inv_fst, pushoutIsoOpPullback_inr_hom, pushoutIsoOpPullback_inl_hom_assoc, op_pullbackMap, pushoutIsoOpPullback_inv_snd
pushoutIsoUnopPullback 📖	CompOp	6 math math: pushoutIsoUnopPullback_inr_hom, pushoutIsoUnopPullback_inl_hom_assoc, pushoutIsoUnopPullback_inr_hom_assoc, pushoutIsoUnopPullback_inv_snd, pushoutIsoUnopPullback_inv_fst, pushoutIsoUnopPullback_inl_hom
spanOp 📖	CompOp	2 math math: spanOp_hom_app, spanOp_inv_app
spanUnop 📖	CompOp	2 math math: spanUnop_inv_app, spanUnop_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cospanOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingCospan WidePullbackShape.category WalkingPair Opposite CategoryTheory.Category.opposite cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.inverse walkingSpanOpEquiv CategoryTheory.Functor.op span CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category cospanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
cospanOp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingCospan WidePullbackShape.category WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.inverse walkingSpanOpEquiv CategoryTheory.Functor.op span cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category cospanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
cospanUnop_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingCospan WidePullbackShape.category WalkingPair cospan Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp Opposite WalkingSpan CategoryTheory.Category.opposite WidePushoutShape.category CategoryTheory.Equivalence.inverse walkingSpanOpEquiv CategoryTheory.Functor.leftOp span CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category cospanUnop CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
cospanUnop_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingCospan WidePullbackShape.category WalkingPair CategoryTheory.Functor.comp Opposite WalkingSpan CategoryTheory.Category.opposite WidePushoutShape.category CategoryTheory.Equivalence.inverse walkingSpanOpEquiv CategoryTheory.Functor.leftOp span cospan Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category cospanUnop CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
hasPullback_op_iff_hasPushout 📖	mathematical	—	HasPullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasPushout	—	HasPullback.eq_1 hasLimit_iff_of_iso hasLimit_inverse_equivalence_comp_iff hasLimit_op_iff_hasColimit
hasPullback_unop_iff_hasPushout 📖	mathematical	—	HasPullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasPushout Opposite CategoryTheory.Category.opposite	—	HasPullback.eq_1 hasLimit_iff_of_iso hasLimit_inverse_equivalence_comp_iff hasLimit_leftOp_iff_hasColimit
hasPullbacks_opposite 📖	mathematical	—	HasPullbacks Opposite CategoryTheory.Category.opposite	—	hasLimitsOfShape_op_of_hasColimitsOfShape hasColimitsOfShape_of_equivalence
hasPushout_op_iff_hasPullback 📖	mathematical	—	HasPushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasPullback	—	HasPushout.eq_1 hasColimit_iff_of_iso hasColimit_inverse_equivalence_comp_iff hasColimit_op_iff_hasLimit
hasPushout_unop_iff_hasPullback 📖	mathematical	—	HasPushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasPullback Opposite CategoryTheory.Category.opposite	—	HasPushout.eq_1 hasColimit_iff_of_iso hasColimit_inverse_equivalence_comp_iff hasColimit_leftOp_iff_hasLimit
hasPushouts_opposite 📖	mathematical	—	HasPushouts Opposite CategoryTheory.Category.opposite	—	hasColimitsOfShape_op_of_hasLimitsOfShape hasLimitsOfShape_of_equivalence
instHasPullbackOppositeOpOfHasPushout 📖	mathematical	—	HasPullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	hasPullback_op_iff_hasPushout
instHasPullbackUnopOfHasPushoutOpposite 📖	mathematical	—	HasPullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	hasPullback_unop_iff_hasPushout
instHasPushoutOppositeOpOfHasPullback 📖	mathematical	—	HasPushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	hasPushout_op_iff_hasPullback
instHasPushoutUnopOfHasPullbackOpposite 📖	mathematical	—	HasPushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	hasPushout_unop_iff_hasPullback
opCospan_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingCospan CategoryTheory.Category.opposite WidePullbackShape.category WalkingPair CategoryTheory.Functor.op cospan CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.functor walkingCospanOpEquiv span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opCospan CategoryTheory.Iso.inv CategoryTheory.Functor.obj Opposite.unop WidePushoutShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opCospan_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingCospan CategoryTheory.Category.opposite WidePullbackShape.category WalkingPair CategoryTheory.Functor.comp WalkingSpan WidePushoutShape.category CategoryTheory.Equivalence.functor walkingCospanOpEquiv span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op cospan CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opCospan CategoryTheory.Iso.hom CategoryTheory.Functor.obj Opposite.unop WidePushoutShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opSpan_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingSpan CategoryTheory.Category.opposite WidePushoutShape.category WalkingPair CategoryTheory.Functor.op span CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.functor walkingSpanOpEquiv cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opSpan CategoryTheory.Iso.inv CategoryTheory.Functor.obj Opposite.unop WidePullbackShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opSpan_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingSpan CategoryTheory.Category.opposite WidePushoutShape.category WalkingPair CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.functor walkingSpanOpEquiv cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op span CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opSpan CategoryTheory.Iso.hom CategoryTheory.Functor.obj Opposite.unop WidePullbackShape CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
op_pullbackMap 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct pullback pullback.map CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.opposite Opposite.op Opposite.unop Quiver.Hom.unop instHasPullbackUnopOfHasPushoutOpposite instHasPushoutOppositeOpOfHasPullback pushout CategoryTheory.Iso.inv pushoutIsoOpPullback pushout.map CategoryTheory.Iso.hom	—	instHasPullbackUnopOfHasPushoutOpposite instHasPushoutOppositeOpOfHasPullback CategoryTheory.Iso.eq_inv_comp pushout.hom_ext pushoutIsoOpPullback_inl_hom_assoc limit.lift_π colimit.ι_desc_assoc CategoryTheory.Category.assoc pushoutIsoOpPullback_inl_hom pushoutIsoOpPullback_inr_hom_assoc pushoutIsoOpPullback_inr_hom
op_pushoutMap 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct pushout pushout.map CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.opposite Opposite.op Opposite.unop Quiver.Hom.unop instHasPushoutUnopOfHasPullbackOpposite instHasPullbackOppositeOpOfHasPushout pullback CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.map CategoryTheory.Iso.hom	—	instHasPushoutUnopOfHasPullbackOpposite instHasPullbackOppositeOpOfHasPushout CategoryTheory.Category.assoc CategoryTheory.Iso.comp_inv_eq pullback.hom_ext pullbackIsoOpPushout_inv_fst colimit.ι_desc limit.lift_π pullbackIsoOpPushout_inv_fst_assoc pullbackIsoOpPushout_inv_snd pullbackIsoOpPushout_inv_snd_assoc
pullbackIsoOpPushout_hom_inl 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pullback Opposite CategoryTheory.Category.opposite pushout.inl Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.fst	—	instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoOpPushout_hom_inl_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pushout.inl pullback Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.fst	—	instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_hom_inl
pullbackIsoOpPushout_hom_inr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pullback Opposite CategoryTheory.Category.opposite pushout.inr Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.snd	—	instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoOpPushout_hom_inr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pushout.inr pullback Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Iso.hom pullbackIsoOpPushout pullback.snd	—	instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_hom_inr
pullbackIsoOpPushout_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pullback CategoryTheory.Category.opposite CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.fst Quiver.Hom.op pushout.inl	—	instHasPushoutUnopOfHasPullbackOpposite IsLimit.conePointUniqueUpToIso_inv_comp CategoryTheory.Category.comp_id
pullbackIsoOpPushout_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pullback CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.fst Quiver.Hom.op pushout.inl	—	instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_inv_fst
pullbackIsoOpPushout_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pullback CategoryTheory.Category.opposite CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.snd Quiver.Hom.op pushout.inr	—	instHasPushoutUnopOfHasPullbackOpposite IsLimit.conePointUniqueUpToIso_inv_comp CategoryTheory.Category.comp_id
pullbackIsoOpPushout_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPushoutUnopOfHasPullbackOpposite pullback CategoryTheory.Iso.inv pullbackIsoOpPushout pullback.snd Quiver.Hom.op pushout.inr	—	instHasPushoutUnopOfHasPullbackOpposite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoOpPushout_inv_snd
pullbackIsoUnopPushout_hom_inl 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pullback pushout.inl Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.fst	—	instHasPushoutOppositeOpOfHasPullback CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoUnopPushout_hom_inl_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pushout.inl pullback Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.fst	—	instHasPushoutOppositeOpOfHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_hom_inl
pullbackIsoUnopPushout_hom_inr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pullback pushout.inr Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.snd	—	instHasPushoutOppositeOpOfHasPullback CategoryTheory.Iso.hom_inv_id_assoc
pullbackIsoUnopPushout_hom_inr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op pushout Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pushout.inr pullback Opposite.unop CategoryTheory.Iso.hom pullbackIsoUnopPushout pullback.snd	—	instHasPushoutOppositeOpOfHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_hom_inr
pullbackIsoUnopPushout_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.fst Quiver.Hom.unop pushout.inl	—	instHasPushoutOppositeOpOfHasPullback IsLimit.conePointUniqueUpToIso_inv_comp PushoutCocone.unop_π_app CategoryTheory.Category.comp_id
pullbackIsoUnopPushout_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.fst Quiver.Hom.unop pushout.inl	—	instHasPushoutOppositeOpOfHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_inv_fst
pullbackIsoUnopPushout_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.snd Quiver.Hom.unop pushout.inr	—	instHasPushoutOppositeOpOfHasPullback IsLimit.conePointUniqueUpToIso_inv_comp PushoutCocone.unop_π_app CategoryTheory.Category.comp_id
pullbackIsoUnopPushout_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPushoutOppositeOpOfHasPullback pullback CategoryTheory.Iso.inv pullbackIsoUnopPushout pullback.snd Quiver.Hom.unop pushout.inr	—	instHasPushoutOppositeOpOfHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoUnopPushout_inv_snd
pushoutIsoOpPullback_inl_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPullbackUnopOfHasPushoutOpposite pushout.inl CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.fst	—	instHasPullbackUnopOfHasPushoutOpposite IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Category.id_comp
pushoutIsoOpPullback_inl_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout pushout.inl Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.fst	—	instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoOpPullback_inl_hom
pushoutIsoOpPullback_inr_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPullbackUnopOfHasPushoutOpposite pushout.inr CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.snd	—	instHasPullbackUnopOfHasPushoutOpposite IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Category.id_comp
pushoutIsoOpPullback_inr_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite pushout pushout.inr Opposite.op pullback Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Iso.hom pushoutIsoOpPullback Quiver.Hom.op pullback.snd	—	instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoOpPullback_inr_hom
pushoutIsoOpPullback_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Iso.inv pushoutIsoOpPullback pullback.fst pushout.inl	—	instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
pushoutIsoOpPullback_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop pushout Opposite CategoryTheory.Category.opposite Opposite.op pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Iso.inv pushoutIsoOpPullback pullback.snd pushout.inr	—	instHasPullbackUnopOfHasPushoutOpposite CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
pushoutIsoUnopPullback_inl_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPullbackOppositeOpOfHasPushout pushout.inl CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.fst	—	instHasPullbackOppositeOpOfHasPushout IsColimit.comp_coconePointUniqueUpToIso_hom PullbackCone.unop_ι_app CategoryTheory.Category.id_comp
pushoutIsoUnopPullback_inl_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout pushout.inl Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPullbackOppositeOpOfHasPushout CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.fst	—	instHasPullbackOppositeOpOfHasPushout CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoUnopPullback_inl_hom
pushoutIsoUnopPullback_inr_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPullbackOppositeOpOfHasPushout pushout.inr CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.snd	—	instHasPullbackOppositeOpOfHasPushout IsColimit.comp_coconePointUniqueUpToIso_hom PullbackCone.unop_ι_app CategoryTheory.Category.id_comp
pushoutIsoUnopPullback_inr_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout pushout.inr Opposite.unop pullback Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPullbackOppositeOpOfHasPushout CategoryTheory.Iso.hom pushoutIsoUnopPullback Quiver.Hom.unop pullback.snd	—	instHasPullbackOppositeOpOfHasPushout CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutIsoUnopPullback_inr_hom
pushoutIsoUnopPullback_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop pullback CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPullbackOppositeOpOfHasPushout CategoryTheory.Iso.inv pushoutIsoUnopPullback pullback.fst pushout.inl	—	instHasPullbackOppositeOpOfHasPushout CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
pushoutIsoUnopPullback_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op pushout Opposite.unop pullback CategoryTheory.Category.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver instHasPullbackOppositeOpOfHasPushout CategoryTheory.Iso.inv pushoutIsoUnopPullback pullback.snd pushout.inr	—	instHasPullbackOppositeOpOfHasPushout CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
spanOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingSpan WidePushoutShape.category WalkingPair Opposite CategoryTheory.Category.opposite span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.inverse walkingCospanOpEquiv CategoryTheory.Functor.op cospan CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category spanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
spanOp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingSpan WidePushoutShape.category WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp WalkingCospan WidePullbackShape.category CategoryTheory.Equivalence.inverse walkingCospanOpEquiv CategoryTheory.Functor.op cospan span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category spanOp CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
spanUnop_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingSpan WidePushoutShape.category WalkingPair span Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp Opposite WalkingCospan CategoryTheory.Category.opposite WidePullbackShape.category CategoryTheory.Equivalence.inverse walkingCospanOpEquiv CategoryTheory.Functor.leftOp cospan CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category spanUnop CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
spanUnop_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingSpan WidePushoutShape.category WalkingPair CategoryTheory.Functor.comp Opposite WalkingCospan CategoryTheory.Category.opposite WidePullbackShape.category CategoryTheory.Equivalence.inverse walkingCospanOpEquiv CategoryTheory.Functor.leftOp cospan span Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category spanUnop CategoryTheory.Functor.obj CategoryTheory.Iso CategoryTheory.Iso.refl	—	—

CategoryTheory.Limits.PullbackCone

Definitions

Name	Category	Theorems
isLimitEquivIsColimitOp 📖	CompOp	—
isLimitEquivIsColimitUnop 📖	CompOp	—
op 📖	CompOp	4 math math: op_pt, op_inr, op_ι_app, op_inl
opUnopIso 📖	CompOp	—
unop 📖	CompOp	4 math math: unop_inl, unop_inr, unop_ι_app, unop_pt
unopOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_inl 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inl Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan fst	—	CategoryTheory.Category.id_comp
op_inr 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inr Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan snd	—	CategoryTheory.Category.id_comp
op_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.cospan	—	—
op_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Equivalence.inverse CategoryTheory.Limits.walkingCospanOpEquiv CategoryTheory.Functor.op CategoryTheory.Limits.cospan CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.Cone.op CategoryTheory.Limits.Cocone.ι op CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.hom CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Limits.Cone.π	—	—
unop_inl 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inl Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan fst	—	unop_ι_app CategoryTheory.Category.id_comp
unop_inr 📖	mathematical	—	CategoryTheory.Limits.PushoutCocone.inr Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan snd	—	unop_ι_app CategoryTheory.Category.id_comp
unop_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan	—	—
unop_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Limits.Cone CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.walkingSpanOpEquiv CategoryTheory.Limits.cospan Opposite.op Quiver.Hom.op CategoryTheory.Limits.Cone.category CategoryTheory.Limits.Cone.postcompose CategoryTheory.Iso.hom CategoryTheory.Iso.symm CategoryTheory.Limits.opSpan CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.Cocone.ι unop CategoryTheory.CategoryStruct.comp CategoryTheory.Iso CategoryTheory.Iso.refl CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.opSpan_inv_app

CategoryTheory.Limits.PushoutCocone

Definitions

Name	Category	Theorems
isColimitEquivIsLimitOp 📖	CompOp	—
isColimitEquivIsLimitUnop 📖	CompOp	—
op 📖	CompOp	4 math math: op_snd, op_π_app, op_pt, op_fst
opUnopIso 📖	CompOp	—
unop 📖	CompOp	4 math math: unop_π_app, unop_pt, unop_snd, unop_fst
unopOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_fst 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.fst Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inl	—	CategoryTheory.Category.comp_id
op_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	—	—
op_snd 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.snd Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span inr	—	CategoryTheory.Category.comp_id
op_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Equivalence.inverse CategoryTheory.Limits.walkingSpanOpEquiv CategoryTheory.Functor.op CategoryTheory.Limits.span CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.Cocone.op CategoryTheory.Limits.cospan Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.π op CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
unop_fst 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.fst Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span inl	—	unop_π_app CategoryTheory.Category.comp_id
unop_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span	—	—
unop_snd 📖	mathematical	—	CategoryTheory.Limits.PullbackCone.snd Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.span inr	—	unop_π_app CategoryTheory.Category.comp_id
unop_π_app 📖	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 Opposite.unop CategoryTheory.Limits.Cocone.pt Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Limits.cospan Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone CategoryTheory.Functor.comp CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Equivalence.functor CategoryTheory.Limits.walkingCospanOpEquiv CategoryTheory.Limits.span Opposite.op Quiver.Hom.op CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocone.precompose CategoryTheory.Iso.hom CategoryTheory.Limits.opCospan CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.Cone.π unop CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv CategoryTheory.Iso CategoryTheory.Iso.refl	—	CategoryTheory.Limits.opCospan_hom_app

---

← Back to Index