Definition is_coprod_enriched_to_Product {a : enriched_coprod_cocone} (Ha : is_coprod_enriched a) (w : C) : Product J V (λ j, E ⦃ D j , w ⦄). Proof. use make_Product. - exact (E ⦃ a , w ⦄). - exact (λ j, precomp_arr E w (enriched_coprod_cocone_in a j)). - exact (Ha w). 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.