Lemma weak_equiv_preserves_pullbacks_unique {q' : D} {qx' : D ⟦ q', F x ⟧} {qy' : D ⟦ q', F y ⟧} (r_q : qx' · # F fₓ = qy' · # F fy) {q : C} (i : z_iso (F q) q') : isaprop (∑ hk : D ⟦ q', F p ⟧, hk · # F pₓ = qx' × hk · # F py = qy'). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro ; apply isapropdirprod ; apply homset_property. } use (cancel_z_iso' i). refine (! homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _ @ _). refine (_ @ homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _). apply maponpaths. use (MorphismsIntoPullbackEqual (pr22 P)). - refine (! homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _). apply maponpaths. simpl. rewrite ! functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } refine (! _). etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } rewrite ! assoc'. apply maponpaths. exact (pr12 φ₂ @ ! (pr12 φ₁)). - refine (! homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _) _). apply maponpaths. simpl. rewrite ! functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } refine (! _). etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (ff_from_weak_equiv _ Fw) _ _)). } rewrite ! assoc'. 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.