Proposition is_prod_enriched_arrow_pr {w : C} (f : ∏ (j : J), w --> D j) (j : J) : is_prod_enriched_arrow f · enriched_prod_cone_pr a j = f j. Proof. unfold is_prod_enriched_arrow, enriched_prod_cone_pr. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn. refine (_ @ ProductPrCommutes _ _ _ (is_prod_enriched_to_Product Ha w) _ (λ j, enriched_from_arr E (f j)) j). cbn. unfold postcomp_arr, enriched_prod_cone_pr. rewrite enriched_from_arr_comp. rewrite !assoc. apply maponpaths_2. rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. rewrite <- tensor_split. rewrite !enriched_from_to_arr. apply idpath. Qed.
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.