Definition weak_equiv_reflect_binproducts_uvp_existence : ∑ fg : C ⟦ x, p ⟧, fg · π₁ = f1 × fg · π₂ = f2. Proof. simple refine (_ ,, _ ,, _). - exact fg. - apply weak_equiv_reflect_binproducts_first_projection_commute. - apply weak_equiv_reflect_binproducts_second_projection_commute. 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.