Lemma weak_equiv_reflects_equalizers : isEqualizer f₁ f₂ h p. Proof. intros e' h' p'. use iscontraprop1. - apply uvp_isEqualizer_isaprop_from_image_weq. exact p'. - use tpair. + use (fully_faithful_inv_hom (ff_from_weak_equiv _ Fw) _ _ _). use (pr11 (iEF (F e') (#F h') _)). abstract (rewrite <- ! functor_comp ; apply maponpaths ; exact p'). + simpl. refine (! homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _). apply maponpaths. simpl. rewrite functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (pr2 Fw) _ _)). } apply (pr21 (iEF _ _ _)). 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.