Definition make_is_prod_enriched_from_underlying (PV : Products J V) (a : enriched_prod_cone) (prod : isProduct J C D a (enriched_prod_cone_pr a)) (HV : conservative_moncat V) : is_prod_enriched a. Proof. use (make_is_prod_enriched_from_z_iso PV). intros w. use HV. use isweq_iso. - exact (prod_from_underlying_arr_map PV a prod w). - exact (prod_from_underlying_arr_map_eq₁ PV a prod w). - exact (prod_from_underlying_arr_map_eq₂ PV a prod w). 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.