Definition weak_equiv_reflects_pullbacks_uvp_existence : ∑ hk : C ⟦ a, p ⟧, hk · pₓ = q₁ × hk · py = q₂. Proof. simple refine (_ ,, _ ,, _). - exact weak_equiv_reflects_pullbacks_uvp_existence₀. - exact weak_equiv_reflects_pullback_uvp_existence_first_projection. - exact weak_equiv_reflects_pullback_uvp_existence_second_projection. 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.