Constructing pullbacks from binary products and equalizers

If a category as binary products and equalizers, then it has pullbacks. Also, if a category has binary coproducts and coequalizers, then it has pushouts

theorem CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g))] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)

If the product X ⨯ Y and the equalizer of π₁ ≫ f and π₂ ≫ g exist, then the pullback of f and g exists: It is given by composing the equalizer with the projections.

theorem CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasPullbacks C

If a category has all binary products and all equalizers, then it also has all pullbacks. As usual, this is not an instance, since there may be a more direct way to construct pullbacks.

theorem CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair Y Z)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr))] : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)

If the coproduct Y ⨿ Z and the coequalizer of f ≫ ι₁ and g ≫ ι₂ exist, then the pushout of f and g exists: It is given by composing the inclusions with the coequalizer.

theorem CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasPushouts C

If a category has all binary coproducts and all coequalizers, then it also has all pushouts. As usual, this is not an instance, since there may be a more direct way to construct pushouts.