Lemma lift_preserves_chosen_pullbacks_uptoeq_after_isotoid_induction : ∥ H (P₂ (G z) (G x) (G y) f' g') = P₃ (H (G z)) (H (G x)) (H (G y)) (# H f') (# H g') ∥. Proof. set (f := (fully_faithful_inv_hom (ff_from_weak_equiv _ Gw) _ _ f')). set (g := (fully_faithful_inv_hom (ff_from_weak_equiv _ Gw) _ _ g')). use (factor_through_squash _ _ (Fpb x y z f g)). { apply isapropishinh. } intro v. set (w := weak_equiv_preserves_pullbacks_eq Gw (pr2 C2) P₁ P₂ x y z f g). use (factor_through_squash _ _ w). { apply isapropishinh. } clear w ; intro w. apply hinhpr. assert (pf_f : #G f = f'). { unfold f ; now rewrite functor_on_fully_faithful_inv_hom. } assert (pf_g : #G g = g'). { unfold g ; now rewrite functor_on_fully_faithful_inv_hom. } rewrite pf_f in w. rewrite pf_g in w. etrans. { apply maponpaths. exact (! w). } clear w. set (ϕ₄ := nat_z_iso_pointwise_z_iso α (P₁ z x y f g)). set (ψ := isotoid _ (pr2 C3) ϕ₄). refine (ψ @ _). refine (v @ _). use (isotoid _ (pr2 C3)). pose (ϕ₁ := nat_z_iso_pointwise_z_iso α x). pose (ϕ₂ := nat_z_iso_pointwise_z_iso α y). pose (ϕ₃ := z_iso_inv (nat_z_iso_pointwise_z_iso α z)). pose (ψ₁ := isotoid _ (pr2 C3) ϕ₁). pose (ψ₂ := isotoid _ (pr2 C3) ϕ₂). pose (ψ₃ := isotoid _ (pr2 C3) ϕ₃). use (Pullback_eq P₃ ψ₁ ψ₂ ψ₃). - rewrite <- pf_f. unfold ψ₁, ψ₃. do 2 rewrite idtoiso_isotoid. etrans. { apply maponpaths_2. exact (! pr21 α _ _ _). } apply z_iso_inv_to_right. apply idpath. - rewrite <- pf_g. unfold ψ₂, ψ₃. do 2 rewrite idtoiso_isotoid. etrans. { apply maponpaths_2. exact (! pr21 α _ _ _). } apply z_iso_inv_to_right. apply idpath. 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.