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