# 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} [𝒞 : ] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd 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.

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} [𝒞 : ] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr))] :

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.

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.