Definition underlying_Product : Product J C D. Proof. use make_Product. - exact a. - exact (enriched_prod_cone_pr a). - intros w f. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; use impred ; intro ; apply homset_property | ] ; exact (is_prod_enriched_arrow_eq (λ j, pr2 φ₁ j @ !(pr2 φ₂ j)))). + exact (is_prod_enriched_arrow f ,, is_prod_enriched_arrow_pr f). 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.Products. Import MonoidalNotations. Section ProductFromUnderlying. End ProductFromUnderlying.