Definition make_is_binary_prod_enriched (a : enriched_binary_prod_cone) (pair : ∏ (w : C) (v : V) (f : v --> E ⦃ w, x ⦄) (g : v --> E ⦃ w, y ⦄), v --> E ⦃ w , a ⦄) (pair_pr1 : ∏ (w : C) (v : V) (f : v --> E ⦃ w, x ⦄) (g : v --> E ⦃ w, y ⦄), pair w v f g · postcomp_arr E w (enriched_prod_cone_pr1 a) = f) (pair_pr2 : ∏ (w : C) (v : V) (f : v --> E ⦃ w, x ⦄) (g : v --> E ⦃ w, y ⦄), pair w v f g · postcomp_arr E w (enriched_prod_cone_pr2 a) = g) (pair_eq : ∏ (w : C) (v : V) (φ₁ φ₂ : v --> E ⦃ w , a ⦄) (q₁ : φ₁ · postcomp_arr E w (enriched_prod_cone_pr1 a) = φ₂ · postcomp_arr E w (enriched_prod_cone_pr1 a)) (q₂ : φ₁ · postcomp_arr E w (enriched_prod_cone_pr2 a) = φ₂ · postcomp_arr E w (enriched_prod_cone_pr2 a)), φ₁ = φ₂) : is_binary_prod_enriched a. Proof. intro w. use make_isBinProduct. intros v f g. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; exact (pair_eq w v (pr1 φ₁) (pr1 φ₂) (pr12 φ₁ @ !(pr12 φ₂)) (pr22 φ₁ @ !(pr22 φ₂)))). - simple refine (_ ,, _ ,, _). + exact (pair w v f g). + exact (pair_pr1 w v f g). + exact (pair_pr2 w v f g). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.BinProducts. Import MonoidalNotations. Section BinaryProductFromUnderlying. End BinaryProductFromUnderlying.