Lemma weak_equiv_lifts_preserves_chosen_pullbacks_eq : preserves_chosen_pullbacks_eq H P₂ P₃. Proof. intros x' y' z' f' g'. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw x')). { apply isapropishinh. } intros [x ix]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y')). { apply isapropishinh. } intros [y iy]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw z')). { apply isapropishinh. } intros [z iz]. induction (isotoid _ (pr2 C2) ix). induction (isotoid _ (pr2 C2) iy). induction (isotoid _ (pr2 C2) iz). exact (lift_preserves_chosen_pullbacks_uptoeq_after_isotoid_induction f' g'). 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.