Lemma weak_equiv_reflects_pullbacks_uvp_uniqueness {a : ob C} {q₁ : C⟦a, x⟧} {q₂ : C⟦a, y⟧} : isaprop (∑ hk : C⟦a, p⟧, hk · pₓ = q₁ × hk · py = q₂). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro; apply isapropdirprod; apply homset_property. } refine (! homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _). apply maponpaths. apply (MorphismsIntoPullbackEqual (pr22 FP)) ; simpl. - rewrite <- ! functor_comp. apply maponpaths. exact (pr12 φ₁ @ ! pr12 φ₂). - rewrite <- ! functor_comp. apply maponpaths. exact (pr22 φ₁ @ ! pr22 φ₂). 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.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation.