Lemma weak_equiv_reflect_binproducts_uvp_uniqueness : isaprop (∑ fg0 : C ⟦ x, p ⟧, fg0 · π₁ = f1 × fg0 · π₂ = f2). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } refine (! homotinvweqweq (weq_from_fully_faithful Fw _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful Fw _ _) _). apply maponpaths. cbn. use (BinProductArrowsEq _ _ _ (make_BinProduct _ _ _ _ _ _ Hp)). - cbn. rewrite <- ! functor_comp. apply maponpaths. exact (pr12 φ₁ @ ! pr12 φ₂). - cbn. rewrite <- ! functor_comp. apply maponpaths. exact (pr22 φ₁ @ ! pr22 φ₂). 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.