Definition preserves_equalizer_equalizer {C₁ C₂ : category} {F : C₁ ⟶ C₂} (HF : preserves_equalizer F) {x y : C₁} {f g : x --> y} (e : Equalizer f g) : Equalizer (#F f) (#F g). Proof. use (make_Equalizer _ _ _ _ (HF _ _ _ _ _ _ _ _ (isEqualizer_Equalizer e))). abstract (rewrite <- !functor_comp ; apply maponpaths ; apply EqualizerEqAr). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Adjunctions.Core.