Commit 2026-08-20 12:19 8ded664b

View on Github →

refactor(CategoryTheory/Limits/Shapes): split up BinaryProducts.lean (#42917) Splits this file (longest file in mathlib at present) into 4 shorter files, and deals with import fallout downstream.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/Basic.lean

Modified Mathlib/CategoryTheory/Comma/Over/Pullback.lean

Modified Mathlib/CategoryTheory/Limits/Connected.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/EpiMono.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Preorder.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/BifunctorCokernel.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

deleted def CategoryTheory.Limits.BinaryCofan.IsColimit.desc'

deleted def CategoryTheory.Limits.BinaryCofan.IsColimit.desc

deleted theorem CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext

deleted theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc

deleted theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc

deleted def CategoryTheory.Limits.BinaryCofan.IsColimit.mk

deleted def CategoryTheory.Limits.BinaryCofan.ext

deleted theorem CategoryTheory.Limits.BinaryCofan.ext_hom_hom

deleted def CategoryTheory.Limits.BinaryCofan.isColimitFlip

deleted def CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv

deleted def CategoryTheory.Limits.BinaryCofan.isColimitMk

deleted theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl

deleted theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr

deleted theorem CategoryTheory.Limits.BinaryCofan.map_inl

deleted theorem CategoryTheory.Limits.BinaryCofan.map_inr

deleted def CategoryTheory.Limits.BinaryCofan.mk

deleted theorem CategoryTheory.Limits.BinaryCofan.mk_inl

deleted theorem CategoryTheory.Limits.BinaryCofan.mk_inr

deleted theorem CategoryTheory.Limits.BinaryCofan.op_mk

deleted theorem CategoryTheory.Limits.BinaryCofan.unop_mk

deleted theorem CategoryTheory.Limits.BinaryCofan.ι_app_left

deleted theorem CategoryTheory.Limits.BinaryCofan.ι_app_right

deleted theorem CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext

deleted def CategoryTheory.Limits.BinaryFan.IsLimit.lift'

deleted def CategoryTheory.Limits.BinaryFan.IsLimit.lift

deleted theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst

deleted theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd

deleted def CategoryTheory.Limits.BinaryFan.IsLimit.mk

deleted def CategoryTheory.Limits.BinaryFan.assoc

deleted def CategoryTheory.Limits.BinaryFan.assocInv

deleted theorem CategoryTheory.Limits.BinaryFan.assocInv_fst

deleted theorem CategoryTheory.Limits.BinaryFan.assocInv_snd

deleted theorem CategoryTheory.Limits.BinaryFan.assoc_fst

deleted theorem CategoryTheory.Limits.BinaryFan.assoc_snd

deleted def CategoryTheory.Limits.BinaryFan.braiding

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd

deleted def CategoryTheory.Limits.BinaryFan.ext

deleted theorem CategoryTheory.Limits.BinaryFan.ext_hom_hom

deleted def CategoryTheory.Limits.BinaryFan.isLimitFlip

deleted def CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv

deleted def CategoryTheory.Limits.BinaryFan.isLimitMk

deleted theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst

deleted theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd

deleted def CategoryTheory.Limits.BinaryFan.leftUnitor

deleted theorem CategoryTheory.Limits.BinaryFan.map_fst

deleted theorem CategoryTheory.Limits.BinaryFan.map_snd

deleted def CategoryTheory.Limits.BinaryFan.mk

deleted theorem CategoryTheory.Limits.BinaryFan.mk_fst

deleted theorem CategoryTheory.Limits.BinaryFan.mk_snd

deleted theorem CategoryTheory.Limits.BinaryFan.op_mk

deleted def CategoryTheory.Limits.BinaryFan.rightUnitor

deleted def CategoryTheory.Limits.BinaryFan.swap

deleted theorem CategoryTheory.Limits.BinaryFan.swap_fst

deleted theorem CategoryTheory.Limits.BinaryFan.swap_snd

deleted theorem CategoryTheory.Limits.BinaryFan.unop_mk

deleted theorem CategoryTheory.Limits.BinaryFan.π_app_left

deleted theorem CategoryTheory.Limits.BinaryFan.π_app_right

deleted theorem CategoryTheory.Limits.HasBinaryProduct.swap

deleted def CategoryTheory.Limits.IsLimit.binaryFanSwap

deleted def CategoryTheory.Limits.WalkingPair.equivBool

deleted theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_left

deleted theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_right

deleted theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false

deleted theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true

deleted def CategoryTheory.Limits.WalkingPair.swap

deleted theorem CategoryTheory.Limits.WalkingPair.swap_apply_left

deleted theorem CategoryTheory.Limits.WalkingPair.swap_apply_right

deleted theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff

deleted theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt

deleted inductive CategoryTheory.Limits.WalkingPair

deleted theorem CategoryTheory.Limits.braid_natural

deleted def CategoryTheory.Limits.coprod.associator

deleted theorem CategoryTheory.Limits.coprod.associator_naturality

deleted def CategoryTheory.Limits.coprod.braiding

deleted theorem CategoryTheory.Limits.coprod.desc_comp

deleted theorem CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr

deleted theorem CategoryTheory.Limits.coprod.desc_inl_inr

deleted theorem CategoryTheory.Limits.coprod.diag_comp

deleted def CategoryTheory.Limits.coprod.functor

deleted def CategoryTheory.Limits.coprod.functorLeftComp

deleted theorem CategoryTheory.Limits.coprod.hom_ext

deleted theorem CategoryTheory.Limits.coprod.inl_desc

deleted theorem CategoryTheory.Limits.coprod.inl_map

deleted theorem CategoryTheory.Limits.coprod.inr_desc

deleted theorem CategoryTheory.Limits.coprod.inr_map

deleted def CategoryTheory.Limits.coprod.leftUnitor

deleted theorem CategoryTheory.Limits.coprod.leftUnitor_naturality

deleted def CategoryTheory.Limits.coprod.mapIso

deleted theorem CategoryTheory.Limits.coprod.map_codiag

deleted theorem CategoryTheory.Limits.coprod.map_comp_id

deleted theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag

deleted theorem CategoryTheory.Limits.coprod.map_desc

deleted theorem CategoryTheory.Limits.coprod.map_id_comp

deleted theorem CategoryTheory.Limits.coprod.map_id_id

deleted theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag

deleted theorem CategoryTheory.Limits.coprod.map_map

deleted theorem CategoryTheory.Limits.coprod.map_swap

deleted theorem CategoryTheory.Limits.coprod.pentagon

deleted def CategoryTheory.Limits.coprod.rightUnitor

deleted theorem CategoryTheory.Limits.coprod.rightUnitor_naturality

deleted theorem CategoryTheory.Limits.coprod.symmetry'

deleted theorem CategoryTheory.Limits.coprod.symmetry

deleted theorem CategoryTheory.Limits.coprod.triangle

deleted def CategoryTheory.Limits.coprodComparison

deleted def CategoryTheory.Limits.coprodComparisonNatIso

deleted def CategoryTheory.Limits.coprodComparisonNatTrans

deleted theorem CategoryTheory.Limits.coprodComparison_inl

deleted theorem CategoryTheory.Limits.coprodComparison_inr

deleted theorem CategoryTheory.Limits.coprodComparison_inv_natural

deleted theorem CategoryTheory.Limits.coprodComparison_natural

deleted def CategoryTheory.Limits.diagramIsoPair

deleted theorem CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair

deleted theorem CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair

deleted theorem CategoryTheory.Limits.inv_prodComparison_map_fst

deleted theorem CategoryTheory.Limits.inv_prodComparison_map_snd

deleted def CategoryTheory.Limits.isoBinaryCofanMk

deleted def CategoryTheory.Limits.isoBinaryFanMk

deleted def CategoryTheory.Limits.mapPair

deleted def CategoryTheory.Limits.mapPairIso

deleted theorem CategoryTheory.Limits.mapPair_left

deleted theorem CategoryTheory.Limits.mapPair_right

deleted theorem CategoryTheory.Limits.map_braiding_hom_comp_prodComparison

deleted theorem CategoryTheory.Limits.map_inl_inv_coprodComparison

deleted theorem CategoryTheory.Limits.map_inr_inv_coprodComparison

deleted def CategoryTheory.Limits.pair

deleted def CategoryTheory.Limits.pairComp

deleted def CategoryTheory.Limits.pairFunction

deleted theorem CategoryTheory.Limits.pairFunction_left

deleted theorem CategoryTheory.Limits.pairFunction_right

deleted theorem CategoryTheory.Limits.pair_obj_left

deleted theorem CategoryTheory.Limits.pair_obj_right

deleted def CategoryTheory.Limits.prod.associator

deleted theorem CategoryTheory.Limits.prod.associator_naturality

deleted def CategoryTheory.Limits.prod.braiding

deleted theorem CategoryTheory.Limits.prod.comp_diag

deleted theorem CategoryTheory.Limits.prod.comp_lift

deleted theorem CategoryTheory.Limits.prod.diag_map

deleted theorem CategoryTheory.Limits.prod.diag_map_fst_snd

deleted theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp

deleted def CategoryTheory.Limits.prod.functor

deleted def CategoryTheory.Limits.prod.functorLeftComp

deleted theorem CategoryTheory.Limits.prod.hom_ext

deleted def CategoryTheory.Limits.prod.leftUnitor

deleted theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality

deleted theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality

deleted theorem CategoryTheory.Limits.prod.lift_fst

deleted theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp

deleted theorem CategoryTheory.Limits.prod.lift_fst_snd

deleted theorem CategoryTheory.Limits.prod.lift_map

deleted theorem CategoryTheory.Limits.prod.lift_snd

deleted def CategoryTheory.Limits.prod.mapIso

deleted theorem CategoryTheory.Limits.prod.map_comp_id

deleted theorem CategoryTheory.Limits.prod.map_fst

deleted theorem CategoryTheory.Limits.prod.map_id_comp

deleted theorem CategoryTheory.Limits.prod.map_id_id

deleted theorem CategoryTheory.Limits.prod.map_map

deleted theorem CategoryTheory.Limits.prod.map_snd

deleted theorem CategoryTheory.Limits.prod.map_swap

deleted theorem CategoryTheory.Limits.prod.pentagon

deleted def CategoryTheory.Limits.prod.rightUnitor

deleted theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality

deleted theorem CategoryTheory.Limits.prod.symmetry'

deleted theorem CategoryTheory.Limits.prod.symmetry

deleted theorem CategoryTheory.Limits.prod.triangle

deleted def CategoryTheory.Limits.prodComparison

deleted def CategoryTheory.Limits.prodComparisonNatIso

deleted def CategoryTheory.Limits.prodComparisonNatTrans

deleted theorem CategoryTheory.Limits.prodComparison_comp

deleted theorem CategoryTheory.Limits.prodComparison_fst

deleted theorem CategoryTheory.Limits.prodComparison_inv_natural

deleted theorem CategoryTheory.Limits.prodComparison_natural

deleted theorem CategoryTheory.Limits.prodComparison_natural_of_natTrans

deleted theorem CategoryTheory.Limits.prodComparison_snd

deleted theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality

Created Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts/BinaryFan.lean

added def CategoryTheory.Limits.BinaryCofan.IsColimit.desc'

added def CategoryTheory.Limits.BinaryCofan.IsColimit.desc

added theorem CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext

added theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc

added theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc

added def CategoryTheory.Limits.BinaryCofan.IsColimit.mk

added def CategoryTheory.Limits.BinaryCofan.ext

added theorem CategoryTheory.Limits.BinaryCofan.ext_hom_hom

added def CategoryTheory.Limits.BinaryCofan.isColimitFlip

added def CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv

added def CategoryTheory.Limits.BinaryCofan.isColimitMk

added theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl

added theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr

added theorem CategoryTheory.Limits.BinaryCofan.map_inl

added theorem CategoryTheory.Limits.BinaryCofan.map_inr

added def CategoryTheory.Limits.BinaryCofan.mk

added theorem CategoryTheory.Limits.BinaryCofan.mk_inl

added theorem CategoryTheory.Limits.BinaryCofan.mk_inr

added theorem CategoryTheory.Limits.BinaryCofan.op_mk

added theorem CategoryTheory.Limits.BinaryCofan.unop_mk

added theorem CategoryTheory.Limits.BinaryCofan.ι_app_left

added theorem CategoryTheory.Limits.BinaryCofan.ι_app_right

added theorem CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext

added def CategoryTheory.Limits.BinaryFan.IsLimit.lift'

added def CategoryTheory.Limits.BinaryFan.IsLimit.lift

added theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst

added theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd

added def CategoryTheory.Limits.BinaryFan.IsLimit.mk

added def CategoryTheory.Limits.BinaryFan.assoc

added def CategoryTheory.Limits.BinaryFan.assocInv

added theorem CategoryTheory.Limits.BinaryFan.assocInv_fst

added theorem CategoryTheory.Limits.BinaryFan.assocInv_snd

added theorem CategoryTheory.Limits.BinaryFan.assoc_fst

added theorem CategoryTheory.Limits.BinaryFan.assoc_snd

added def CategoryTheory.Limits.BinaryFan.braiding

added theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst

added theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd

added theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst

added theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd

added def CategoryTheory.Limits.BinaryFan.ext

added theorem CategoryTheory.Limits.BinaryFan.ext_hom_hom

added def CategoryTheory.Limits.BinaryFan.isLimitFlip

added def CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv

added def CategoryTheory.Limits.BinaryFan.isLimitMk

added theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst

added theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd

added def CategoryTheory.Limits.BinaryFan.leftUnitor

added theorem CategoryTheory.Limits.BinaryFan.map_fst

added theorem CategoryTheory.Limits.BinaryFan.map_snd

added def CategoryTheory.Limits.BinaryFan.mk

added theorem CategoryTheory.Limits.BinaryFan.mk_fst

added theorem CategoryTheory.Limits.BinaryFan.mk_snd

added theorem CategoryTheory.Limits.BinaryFan.op_mk

added def CategoryTheory.Limits.BinaryFan.rightUnitor

added def CategoryTheory.Limits.BinaryFan.swap

added theorem CategoryTheory.Limits.BinaryFan.swap_fst

added theorem CategoryTheory.Limits.BinaryFan.swap_snd

added theorem CategoryTheory.Limits.BinaryFan.unop_mk

added theorem CategoryTheory.Limits.BinaryFan.π_app_left

added theorem CategoryTheory.Limits.BinaryFan.π_app_right

added def CategoryTheory.Limits.IsLimit.binaryFanSwap

added def CategoryTheory.Limits.isoBinaryCofanMk

added def CategoryTheory.Limits.isoBinaryFanMk

Created Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts/BinaryProducts.lean

added theorem CategoryTheory.Limits.HasBinaryProduct.swap

added theorem CategoryTheory.Limits.braid_natural

added def CategoryTheory.Limits.coprod.associator

added theorem CategoryTheory.Limits.coprod.associator_naturality

added def CategoryTheory.Limits.coprod.braiding

added theorem CategoryTheory.Limits.coprod.desc_comp

added theorem CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr

added theorem CategoryTheory.Limits.coprod.desc_inl_inr

added theorem CategoryTheory.Limits.coprod.diag_comp

added def CategoryTheory.Limits.coprod.functor

added def CategoryTheory.Limits.coprod.functorLeftComp

added theorem CategoryTheory.Limits.coprod.hom_ext

added theorem CategoryTheory.Limits.coprod.inl_desc

added theorem CategoryTheory.Limits.coprod.inl_map

added theorem CategoryTheory.Limits.coprod.inr_desc

added theorem CategoryTheory.Limits.coprod.inr_map

added def CategoryTheory.Limits.coprod.leftUnitor

added theorem CategoryTheory.Limits.coprod.leftUnitor_naturality

added def CategoryTheory.Limits.coprod.mapIso

added theorem CategoryTheory.Limits.coprod.map_codiag

added theorem CategoryTheory.Limits.coprod.map_comp_id

added theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag

added theorem CategoryTheory.Limits.coprod.map_desc

added theorem CategoryTheory.Limits.coprod.map_id_comp

added theorem CategoryTheory.Limits.coprod.map_id_id

added theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag

added theorem CategoryTheory.Limits.coprod.map_map

added theorem CategoryTheory.Limits.coprod.map_swap

added theorem CategoryTheory.Limits.coprod.pentagon

added def CategoryTheory.Limits.coprod.rightUnitor

added theorem CategoryTheory.Limits.coprod.rightUnitor_naturality

added theorem CategoryTheory.Limits.coprod.symmetry'

added theorem CategoryTheory.Limits.coprod.symmetry

added theorem CategoryTheory.Limits.coprod.triangle

added theorem CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair

added theorem CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair

added def CategoryTheory.Limits.prod.associator

added theorem CategoryTheory.Limits.prod.associator_naturality

added def CategoryTheory.Limits.prod.braiding

added theorem CategoryTheory.Limits.prod.comp_diag

added theorem CategoryTheory.Limits.prod.comp_lift

added theorem CategoryTheory.Limits.prod.diag_map

added theorem CategoryTheory.Limits.prod.diag_map_fst_snd

added theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp

added def CategoryTheory.Limits.prod.functor

added def CategoryTheory.Limits.prod.functorLeftComp

added theorem CategoryTheory.Limits.prod.hom_ext

added def CategoryTheory.Limits.prod.leftUnitor

added theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality

added theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality

added theorem CategoryTheory.Limits.prod.lift_fst

added theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp

added theorem CategoryTheory.Limits.prod.lift_fst_snd

added theorem CategoryTheory.Limits.prod.lift_map

added theorem CategoryTheory.Limits.prod.lift_snd

added def CategoryTheory.Limits.prod.mapIso

added theorem CategoryTheory.Limits.prod.map_comp_id

added theorem CategoryTheory.Limits.prod.map_fst

added theorem CategoryTheory.Limits.prod.map_id_comp

added theorem CategoryTheory.Limits.prod.map_id_id

added theorem CategoryTheory.Limits.prod.map_map

added theorem CategoryTheory.Limits.prod.map_snd

added theorem CategoryTheory.Limits.prod.map_swap

added theorem CategoryTheory.Limits.prod.pentagon

added def CategoryTheory.Limits.prod.rightUnitor

added theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality

added theorem CategoryTheory.Limits.prod.symmetry'

added theorem CategoryTheory.Limits.prod.symmetry

added theorem CategoryTheory.Limits.prod.triangle

added theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality

Created Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts/ProdComparison.lean

added def CategoryTheory.Limits.coprodComparison

added def CategoryTheory.Limits.coprodComparisonNatIso

added def CategoryTheory.Limits.coprodComparisonNatTrans

added theorem CategoryTheory.Limits.coprodComparison_inl

added theorem CategoryTheory.Limits.coprodComparison_inr

added theorem CategoryTheory.Limits.coprodComparison_inv_natural

added theorem CategoryTheory.Limits.coprodComparison_natural

added theorem CategoryTheory.Limits.inv_prodComparison_map_fst

added theorem CategoryTheory.Limits.inv_prodComparison_map_snd

added theorem CategoryTheory.Limits.map_braiding_hom_comp_prodComparison

added theorem CategoryTheory.Limits.map_inl_inv_coprodComparison

added theorem CategoryTheory.Limits.map_inr_inv_coprodComparison

added def CategoryTheory.Limits.prodComparison

added def CategoryTheory.Limits.prodComparisonNatIso

added def CategoryTheory.Limits.prodComparisonNatTrans

added theorem CategoryTheory.Limits.prodComparison_comp

added theorem CategoryTheory.Limits.prodComparison_fst

added theorem CategoryTheory.Limits.prodComparison_inv_natural

added theorem CategoryTheory.Limits.prodComparison_natural

added theorem CategoryTheory.Limits.prodComparison_natural_of_natTrans

added theorem CategoryTheory.Limits.prodComparison_snd

Created Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts/WalkingPair.lean

added def CategoryTheory.Limits.WalkingPair.equivBool

added theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_left

added theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_right

added theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false

added theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true

added def CategoryTheory.Limits.WalkingPair.swap

added theorem CategoryTheory.Limits.WalkingPair.swap_apply_left

added theorem CategoryTheory.Limits.WalkingPair.swap_apply_right

added theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff

added theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt

added inductive CategoryTheory.Limits.WalkingPair

added def CategoryTheory.Limits.diagramIsoPair

added def CategoryTheory.Limits.mapPair

added def CategoryTheory.Limits.mapPairIso

added theorem CategoryTheory.Limits.mapPair_left

added theorem CategoryTheory.Limits.mapPair_right

added def CategoryTheory.Limits.pair

added def CategoryTheory.Limits.pairComp

added def CategoryTheory.Limits.pairFunction

added theorem CategoryTheory.Limits.pairFunction_left

added theorem CategoryTheory.Limits.pairFunction_right

added theorem CategoryTheory.Limits.pair_obj_left

added theorem CategoryTheory.Limits.pair_obj_right

Modified Mathlib/CategoryTheory/Limits/Shapes/CombinedProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

Modified Mathlib/CategoryTheory/Limits/Types/Coproducts.lean

Modified Mathlib/CategoryTheory/Limits/Types/Products.lean

Modified Mathlib/CategoryTheory/Monad/Products.lean

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

Modified Mathlib/CategoryTheory/Subterminal.lean