Definition preserves_equalizer_if_preserves_chosen {C₁ C₂ : category} (HC₁ : Equalizers C₁) (F : C₁ ⟶ C₂) (HF : preserves_chosen_equalizer HC₁ F) : preserves_equalizer F. Proof. intros x y e f g h p Fp H. use (isEqualizer_z_iso (HF x y f g _) (functor_on_z_iso F (z_iso_from_Equalizer_to_Equalizer (make_Equalizer _ _ _ _ H) (HC₁ x y f g)))). - abstract (rewrite <- !functor_comp ; apply maponpaths ; apply EqualizerEqAr). - abstract (cbn ; rewrite <- functor_comp ; apply maponpaths ; refine (!_) ; unfold from_Equalizer_to_Equalizer ; apply EqualizerCommutes). 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.