Corollary weak_equiv_preserves_chosen_pullbacks {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (PB : Pullbacks C) : preserves_chosen_pullback PB F. Proof. intros x y f g p. use (weak_equiv_preserves_pullbacks Fw). - apply PullbackSqrCommutes. - apply isPullback_Pullback. 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.