Definition is_prod_enriched_arrow {w : C} (f : ∏ (j : J), w --> D j) : w --> a. Proof. refine (enriched_to_arr E _). use (ProductArrow _ _ (is_prod_enriched_to_Product Ha w)). exact (λ j, enriched_from_arr E (f j)). 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.