Lemma weak_equiv_lifts_preserves_pullbacks : preserves_pullback H. Proof. intros y1 y2 py' py fy gy π₁y π₂y q Fq ispby. set (PB := make_Pullback _ ispby). use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y1)). { apply isaprop_isPullback. } intros [x1 i1]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y2)). { apply isaprop_isPullback. } intros [x2 i2]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw py)). { apply isaprop_isPullback. } intros [px i]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw py')). { apply isaprop_isPullback. } intros [px' i']. exact (pullback_is_preserved_after_lift ispby i1 i2 i i'). 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. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Pullbacks. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Pullbacks.