Proposition prod_from_underlying_arr_map_eq₁ (f : I_{V} --> E ⦃ w, a ⦄) : prod_from_underlying_arr_map (f · prod_enriched_to_prod PV a w) = f. Proof. unfold prod_from_underlying_arr_map. refine (_ @ enriched_from_to_arr E f). apply maponpaths. use (ProductArrow_eq _ _ _ (make_Product _ _ _ _ _ prod)). unfold prod_enriched_to_prod. intro j. rewrite ProductPrCommutes ; cbn. rewrite (enriched_to_arr_comp E). apply maponpaths. rewrite tensor_split. rewrite !assoc. rewrite <- tensor_linvunitor. rewrite !assoc'. rewrite enriched_from_to_arr. apply maponpaths. rewrite !assoc. etrans. { apply (ProductPrCommutes _ _ _ (PV (λ k, E ⦃ w , D k ⦄)) _ _ j). } 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.