Proposition coprod_from_underlying_arr_map_eq₁ (f : I_{V} --> E ⦃ a , w ⦄) : coprod_from_underlying_arr_map (f · coprod_enriched_to_prod PV a w) = f. Proof. unfold coprod_from_underlying_arr_map. refine (_ @ enriched_from_to_arr E f). apply maponpaths. use (CoproductArrow_eq _ _ _ (make_Coproduct _ _ _ _ _ coprod)). unfold coprod_enriched_to_prod. intro j. rewrite CoproductInCommutes ; cbn. rewrite (enriched_to_arr_comp E). apply maponpaths. rewrite !assoc'. etrans. { apply maponpaths. apply (ProductPrCommutes _ _ _ (PV (λ k, E ⦃ D k , w ⦄)) _ _ j). } unfold precomp_arr. rewrite !assoc. rewrite tensor_rinvunitor. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite enriched_from_to_arr. 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.Products. Require Import UniMath.CategoryTheory.Limits.Coproducts. Import MonoidalNotations. Section CoproductFromUnderlying. End CoproductFromUnderlying.