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