Corollary weak_equiv_preserves_pullbacks_eq {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (Duniv : is_univalent D) (P₁ : Pullbacks C) (P₂ : Pullbacks D) : preserves_chosen_pullbacks_eq F P₁ P₂. Proof. intros x y z f g. apply hinhpr. apply Duniv. set (Fp := weak_equiv_preserves_pullbacks Fw). use (z_iso_from_Pullback_to_Pullback (make_Pullback _ (Fp _ _ _ _ _ _ _ _ _ _ (pr22 (P₁ _ _ _ _ _)))) (P₂ _ _ _ (#F f) (#F g))). do 2 rewrite <- functor_comp. apply maponpaths. apply P₁. 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.