Proposition is_prod_enriched_arrow_eq {w : C} {f g : w --> a} (q : ∏ (j : J), f · enriched_prod_cone_pr a j = g · enriched_prod_cone_pr a j) : f = g. Proof. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. use (ProductArrow_eq _ _ _ (is_prod_enriched_to_Product Ha w)). intro j. cbn. unfold postcomp_arr. rewrite !assoc. rewrite !tensor_linvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite <- !(enriched_to_arr_comp E). exact (q j). 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.