Lemma uvp_isEqualizer_isaprop_from_image_weq {e' : C} {h' : C ⟦ e', x ⟧} (p' : h' · f₁ = h' · f₂) : isaprop (∑ φ : C ⟦ e', e ⟧, φ · h = h'). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro; apply homset_property. } refine (! homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _). apply maponpaths. cbn. apply (EqualizerInsEq (make_Equalizer _ _ _ _ iEF)). cbn. rewrite <- ! functor_comp. apply maponpaths. exact (pr2 φ₁ @ ! pr2 φ₂). 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.