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