Lemma weak_equiv_reflects_pullback_uvp_existence_second_projection : weak_equiv_reflects_pullbacks_uvp_existence₀ · py = q₂. Proof. simpl. refine (! homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful (pr2 Fw) _ _) _). apply maponpaths. simpl. rewrite functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful (pr2 Fw) _ _)). } apply (pr21 (iFP _ _ _ _)). 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.