Proposition weak_equiv_preserves_pullbacks {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) : preserves_pullback F. Proof. intros x y z p fₓ fy pₓ py r_p Fr_p iP. pose (P := make_Pullback _ iP). intros q' qx' qy' r_q. use (factor_through_squash (isapropiscontr _) _ (eso_from_weak_equiv _ Fw q')). intros [q i]. transparent assert (e : (D⟦q', F p⟧)). { use (z_iso_inv i · #F (pr11 (iP _ _ _ _))). + apply (fully_faithful_inv_hom (ff_from_weak_equiv _ Fw)). exact (i · qx'). + apply (fully_faithful_inv_hom (ff_from_weak_equiv _ Fw)). exact (i · qy'). + abstract (use (faithful_reflects_morphism_equality F (pr2 Fw)) ; do 2 rewrite functor_comp ; do 2 rewrite functor_on_fully_faithful_inv_hom ; do 2 rewrite assoc' ; apply maponpaths ; exact r_q). } assert (e₁ : e · # F pₓ = qx'). { refine (assoc' _ _ _ @ _). rewrite <- (functor_comp F). etrans. { do 2 apply maponpaths. exact (pr121 (iP _ _ _ _)). } etrans. { apply maponpaths. apply functor_on_fully_faithful_inv_hom. } rewrite assoc. etrans. { apply maponpaths_2. apply z_iso_after_z_iso_inv. } apply id_left. } assert (e₂ : e · # F py = qy'). { refine (assoc' _ _ _ @ _). rewrite <- (functor_comp F). etrans. { do 2 apply maponpaths. exact (pr221 (iP _ _ _ _)). } etrans. { apply maponpaths. apply functor_on_fully_faithful_inv_hom. } rewrite assoc. etrans. { apply maponpaths_2. apply z_iso_after_z_iso_inv. } apply id_left. } apply (iscontraprop1 (weak_equiv_preserves_pullbacks_unique Fw iP r_q i)). exact (e ,, (e₁ ,, e₂)). 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.