Definition weak_equiv_reflects_pullbacks_uvp_existence₀ : C ⟦ a, p ⟧. Proof. use (fully_faithful_inv_hom (ff_from_weak_equiv _ Fw) _ _ _). use (pr11 (iFP (F _) (#F q₁) (#F q₂) _)). abstract (rewrite <- ! functor_comp ; apply maponpaths ; exact 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.