Proposition weak_equiv_preserves_equalizers {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) : preserves_equalizer F. Proof. intros x y e f₁ f₂ h p Fp iE. pose (E := make_Equalizer _ _ _ _ iE). intros e' h' p'. use (factor_through_squash (isapropiscontr _) _ (eso_from_weak_equiv _ Fw e')). intros [e'' i]. apply (iscontraprop1 (weak_equiv_preserves_equalizers_unique Fw iE h' i)). set (ϕ := fully_faithful_inv_hom (ff_from_weak_equiv _ Fw) _ _ (i · h')). assert (q : ϕ · f₁ = ϕ · f₂). { use (faithful_reflects_morphism_equality F (pr2 Fw)). do 2 rewrite functor_comp. unfold ϕ. rewrite functor_on_fully_faithful_inv_hom. do 2 rewrite assoc'. apply maponpaths. exact p'. } exists (z_iso_inv i · #F (pr11 (iE _ _ q))). rewrite assoc'. rewrite <- (functor_comp F). etrans. { do 2 apply maponpaths. exact (pr21 (iE _ _ q)). } etrans. { apply maponpaths. apply functor_on_fully_faithful_inv_hom. } rewrite assoc. etrans. { apply maponpaths_2. apply z_iso_after_z_iso_inv. } apply id_left. 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.