Proposition prod_from_underlying_arr_map_eq₁ (f : I_{V} --> E ⦃ w, a ⦄) : prod_from_underlying_arr_map (f · binary_prod_enriched_to_prod BPV a w) = f. Proof. unfold prod_from_underlying_arr_map. refine (_ @ enriched_from_to_arr E f). apply maponpaths. use (BinProductArrowsEq _ _ _ (make_BinProduct C x y a _ _ prod)). - unfold binary_prod_enriched_to_prod. rewrite !assoc'. rewrite !BinProductPr1Commutes ; 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. apply idpath. - unfold binary_prod_enriched_to_prod. rewrite !assoc'. rewrite !BinProductPr2Commutes ; 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. 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.BinProducts. Import MonoidalNotations. Section BinaryProductFromUnderlying. End BinaryProductFromUnderlying.