Definition is_prod_enriched_to_Product {a : enriched_prod_cone} (Ha : is_prod_enriched a) (w : C) : Product J V (λ j, E ⦃ w , D j ⦄). Proof. use make_Product. - exact (E ⦃ w , a ⦄). - exact (λ j, postcomp_arr E w (enriched_prod_cone_pr a j)). - exact (Ha 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.