Lemma weak_equiv_reflects_pullbacks : isPullback r. Proof. intros a q₁ q₂ r'. use iscontraprop1. - apply weak_equiv_reflects_pullbacks_uvp_uniqueness. - exact (weak_equiv_reflects_pullbacks_uvp_existence r'). Defined.
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.