Definition underlying_BinProduct : BinProduct C x y. Proof. use make_BinProduct. - exact a. - exact (enriched_prod_cone_pr1 a). - exact (enriched_prod_cone_pr2 a). - intros w f g. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; exact (is_binary_prod_enriched_arrow_eq (pr12 φ₁ @ !(pr12 φ₂)) (pr22 φ₁ @ !(pr22 φ₂)))). + exact (is_binary_prod_enriched_arrow f g ,, is_binary_prod_enriched_arrow_pr1 f g ,, is_binary_prod_enriched_arrow_pr2 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.