Equalizers as pullbacks of products

Also see CategoryTheory.Limits.Constructions.Equalizers for very similar results.

theorem CategoryTheory.Limits.isPullback_equalizer_prod {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasBinaryProduct Y Y] : CategoryTheory.IsPullback (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f) (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))

The equalizer of f g : X ⟶ Y is the pullback of the diagonal map Y ⟶ Y × Y along the map (f, g) : X ⟶ Y × Y.

theorem CategoryTheory.Limits.isPushout_coequalizer_coprod {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Limits.HasBinaryCoproduct X X] : CategoryTheory.IsPushout (CategoryTheory.Limits.coprod.desc f g) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.coequalizer.π f g))

The coequalizer of f g : X ⟶ Y is the pushout of the diagonal map X ⨿ X ⟶ X along the map (f, g) : X ⨿ X ⟶ Y.