Equalizers

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

Statistics

Metric	Count
Definitions isColimitCoforkPushoutEquivIsColimitForkOpPullback, isColimitCoforkPushoutEquivIsColimitForkUnopPullback, isColimitEquivIsLimitOp, isColimitEquivIsLimitUnop, isColimitOfπEquivIsLimitOp, isColimitOfπEquivIsLimitUnop, ofπOpIsoOfι, ofπUnopIsoOfι, op, opUnopIso, unop, unopOpIso, isLimitEquivIsColimitOp, isLimitEquivIsColimitUnop, isLimitForkPushoutEquivIsColimitForkOpPullback, isLimitForkPushoutEquivIsColimitForkUnopPullback, isLimitOfιEquivIsColimitOp, isLimitOfιEquivIsColimitUnop, ofιOpIsoOfπ, ofιUnopIsoOfπ, op, opUnopIso, unop, unopOpIso, opParallelPairIso, parallelPairOpIso	26
Theorems op_unop_π, op_ι, op_π_app_one, op_π_app_zero, unop_op_π, unop_ι, unop_π_app_one, unop_π_app_zero, op_pt, op_unop_ι, op_ι_app, op_ι_app_one, op_ι_app_zero, op_π, unop_op_ι, unop_ι_app_one, unop_ι_app_zero, unop_π, hasCoequalizers_opposite, hasEqualizers_opposite, opParallelPairIso_hom_app_one, opParallelPairIso_hom_app_zero, opParallelPairIso_inv_app_one, opParallelPairIso_inv_app_zero, parallelPairOpIso_hom_app_one, parallelPairOpIso_hom_app_zero, parallelPairOpIso_inv_app_one, parallelPairOpIso_inv_app_zero	28
Total	54

CategoryTheory.Limits

Definitions

Name	Category	Theorems
opParallelPairIso 📖	CompOp	4 math math: opParallelPairIso_hom_app_zero, opParallelPairIso_hom_app_one, opParallelPairIso_inv_app_zero, opParallelPairIso_inv_app_one
parallelPairOpIso 📖	CompOp	5 math math: parallelPairOpIso_inv_app_zero, parallelPairOpIso_inv_app_one, parallelPairOpIso_hom_app_one, Fork.op_ι_app, parallelPairOpIso_hom_app_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCoequalizers_opposite 📖	mathematical	—	HasCoequalizers Opposite CategoryTheory.Category.opposite	—	hasColimitsOfShape_op_of_hasLimitsOfShape hasLimitsOfShape_of_equivalence
hasEqualizers_opposite 📖	mathematical	—	HasEqualizers Opposite CategoryTheory.Category.opposite	—	hasLimitsOfShape_op_of_hasColimitsOfShape hasColimitsOfShape_of_equivalence
opParallelPairIso_hom_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingParallelPair CategoryTheory.Category.opposite walkingParallelPairHomCategory CategoryTheory.Functor.op parallelPair CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse walkingParallelPairOpEquiv Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opParallelPairIso WalkingParallelPair.one CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	CategoryTheory.Iso.refl_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opParallelPairIso_hom_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingParallelPair CategoryTheory.Category.opposite walkingParallelPairHomCategory CategoryTheory.Functor.op parallelPair CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse walkingParallelPairOpEquiv Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category opParallelPairIso WalkingParallelPair.zero CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	CategoryTheory.Iso.refl_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opParallelPairIso_inv_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingParallelPair CategoryTheory.Category.opposite walkingParallelPairHomCategory CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse walkingParallelPairOpEquiv parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opParallelPairIso WalkingParallelPair.one CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	CategoryTheory.Iso.refl_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
opParallelPairIso_inv_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WalkingParallelPair CategoryTheory.Category.opposite walkingParallelPairHomCategory CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse walkingParallelPairOpEquiv parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category opParallelPairIso WalkingParallelPair.zero CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	CategoryTheory.Iso.refl_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Category.assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
parallelPairOpIso_hom_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingParallelPair walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor walkingParallelPairOpEquiv CategoryTheory.Functor.op CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category parallelPairOpIso WalkingParallelPair.one CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	—
parallelPairOpIso_hom_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingParallelPair walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor walkingParallelPairOpEquiv CategoryTheory.Functor.op CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category parallelPairOpIso WalkingParallelPair.zero CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	—
parallelPairOpIso_inv_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingParallelPair walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor walkingParallelPairOpEquiv CategoryTheory.Functor.op parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category parallelPairOpIso WalkingParallelPair.one CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	—
parallelPairOpIso_inv_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app WalkingParallelPair walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor walkingParallelPairOpEquiv CategoryTheory.Functor.op parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category parallelPairOpIso WalkingParallelPair.zero CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.obj	—	—

CategoryTheory.Limits.Cofork

Definitions

Name	Category	Theorems
isColimitCoforkPushoutEquivIsColimitForkOpPullback 📖	CompOp	—
isColimitCoforkPushoutEquivIsColimitForkUnopPullback 📖	CompOp	—
isColimitEquivIsLimitOp 📖	CompOp	—
isColimitEquivIsLimitUnop 📖	CompOp	—
isColimitOfπEquivIsLimitOp 📖	CompOp	—
isColimitOfπEquivIsLimitUnop 📖	CompOp	—
ofπOpIsoOfι 📖	CompOp	—
ofπUnopIsoOfι 📖	CompOp	—
op 📖	CompOp	5 math math: CategoryTheory.Limits.Fork.unop_op_ι, op_π_app_zero, op_unop_π, op_π_app_one, op_ι
opUnopIso 📖	CompOp	—
unop 📖	CompOp	5 math math: unop_op_π, unop_π_app_one, unop_π_app_zero, CategoryTheory.Limits.Fork.op_unop_ι, unop_ι
unopOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_unop_π 📖	mathematical	—	π Opposite.unop Opposite.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.op CategoryTheory.Limits.Fork.unop op	—	CategoryTheory.Limits.Fork.unop_π op_ι
op_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt π	—	CategoryTheory.Category.comp_id
op_π_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	app_zero_eq_comp_π_left CategoryTheory.Category.comp_id
op_π_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Category.comp_id
unop_op_π 📖	mathematical	—	π Opposite CategoryTheory.Category.opposite Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop CategoryTheory.Limits.Fork.op unop	—	CategoryTheory.Limits.Fork.op_π unop_ι
unop_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.parallelPair CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt π	—	CategoryTheory.Limits.opParallelPairIso_hom_app_zero CategoryTheory.Category.id_comp
unop_π_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.one Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Limits.opParallelPairIso_hom_app_one app_zero_eq_comp_π_left CategoryTheory.Category.id_comp
unop_π_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.zero Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Limits.opParallelPairIso_hom_app_zero CategoryTheory.Category.id_comp

CategoryTheory.Limits.Fork

Definitions

Name	Category	Theorems
isLimitEquivIsColimitOp 📖	CompOp	—
isLimitEquivIsColimitUnop 📖	CompOp	—
isLimitForkPushoutEquivIsColimitForkOpPullback 📖	CompOp	—
isLimitForkPushoutEquivIsColimitForkUnopPullback 📖	CompOp	—
isLimitOfιEquivIsColimitOp 📖	CompOp	—
isLimitOfιEquivIsColimitUnop 📖	CompOp	—
ofιOpIsoOfπ 📖	CompOp	—
ofιUnopIsoOfπ 📖	CompOp	—
op 📖	CompOp	7 math math: CategoryTheory.Limits.Cofork.unop_op_π, op_pt, op_π, op_ι_app, op_ι_app_one, op_ι_app_zero, op_unop_ι
opUnopIso 📖	CompOp	—
unop 📖	CompOp	5 math math: unop_ι_app_zero, unop_ι_app_one, unop_op_ι, CategoryTheory.Limits.Cofork.op_unop_π, unop_π
unopOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.parallelPair Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Limits.Cone.pt	—	—
op_unop_ι 📖	mathematical	—	ι Opposite.unop Opposite.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.op CategoryTheory.Limits.Cofork.unop op	—	CategoryTheory.Limits.Cofork.unop_ι op_π
op_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.parallelPair 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.Equivalence.functor CategoryTheory.Limits.walkingParallelPairOpEquiv CategoryTheory.Functor.op CategoryTheory.Limits.Cocone.whisker CategoryTheory.Limits.Cone.op CategoryTheory.Limits.Cocone.ι op CategoryTheory.CategoryStruct.comp Opposite.unop CategoryTheory.Limits.walkingParallelPairOp CategoryTheory.Limits.Cone.pt CategoryTheory.Iso.hom CategoryTheory.Limits.parallelPairOpIso CategoryTheory.Limits.Cone.π	—	—
op_ι_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.parallelPair 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 op CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.id_comp
op_ι_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.parallelPair 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 op CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Cone.π	—	app_one_eq_ι_comp_left CategoryTheory.Category.id_comp
op_π 📖	mathematical	—	CategoryTheory.Limits.Cofork.π Opposite CategoryTheory.Category.opposite Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct op CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.Limits.WalkingParallelPair.zero ι	—	CategoryTheory.Category.id_comp
unop_op_ι 📖	mathematical	—	ι Opposite CategoryTheory.Category.opposite Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop CategoryTheory.Limits.Cofork.op unop	—	CategoryTheory.Limits.Cofork.op_ι unop_π
unop_ι_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt unop CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingParallelPair.one Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.opParallelPairIso_inv_app_one CategoryTheory.Category.comp_id
unop_ι_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt unop CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingParallelPair.zero Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Cone.π	—	app_one_eq_ι_comp_left CategoryTheory.Limits.opParallelPairIso_inv_app_zero CategoryTheory.Category.comp_id
unop_π 📖	mathematical	—	CategoryTheory.Limits.Cofork.π Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unop CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.Limits.WalkingParallelPair.zero ι	—	CategoryTheory.Limits.opParallelPairIso_inv_app_one CategoryTheory.Category.comp_id

---

← Back to Index