proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.Limits.Products