Corollary weak_equiv_preserves_chosen_equalizers {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (BP : Equalizers C) : preserves_chosen_equalizer BP F. Proof. intros x y f g p. use (weak_equiv_preserves_equalizers Fw). - apply EqualizerEqAr. - apply isEqualizer_Equalizer. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Preservation.