Proposition coprod_from_underlying_arr_map_eq₂ (f : I_{V} --> BPV (E ⦃ x , w ⦄) (E ⦃ y , w ⦄)) : coprod_from_underlying_arr_map f · binary_coprod_enriched_to_coprod BPV a w = f. Proof. unfold coprod_from_underlying_arr_map. use (BinProductArrowsEq _ _ _ (BPV (E ⦃ x , w ⦄) (E ⦃ y , w ⦄))). - unfold binary_coprod_enriched_to_coprod. rewrite !assoc'. rewrite !BinProductPr1Commutes. rewrite enriched_from_arr_precomp. refine (_ @ enriched_from_to_arr E _). apply maponpaths. apply (BinCoproductIn1Commutes _ _ _ (make_BinCoproduct C x y a _ _ coprod)). - unfold binary_coprod_enriched_to_coprod. rewrite !assoc'. rewrite !BinProductPr2Commutes. rewrite enriched_from_arr_precomp. refine (_ @ enriched_from_to_arr E _). apply maponpaths. apply (BinCoproductIn2Commutes _ _ _ (make_BinCoproduct C x y a _ _ coprod)). 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. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Import MonoidalNotations. Section BinaryCoproductFromUnderlying. End BinaryCoproductFromUnderlying.