Definition coprod_from_underlying_arr_map (f : I_{V} --> PV (λ j, E ⦃ D j , w ⦄)) : I_{V} --> E ⦃ a , w ⦄. Proof. apply enriched_from_arr. use (CoproductArrow _ _ (make_Coproduct _ _ _ _ _ coprod)). intro j. exact (enriched_to_arr E (f · ProductPr _ _ _ j)). Defined.
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.