Definition binary_coprod_enriched_to_coprod (BPV : BinProducts V) (a : enriched_binary_coprod_cocone) (w : C) : E ⦃ a , w ⦄ --> BPV (E ⦃ x , w ⦄) (E ⦃ y , w ⦄). Proof. use BinProductArrow. - exact (precomp_arr E w (enriched_coprod_cocone_in1 a)). - exact (precomp_arr E w (enriched_coprod_cocone_in2 a)). 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Import MonoidalNotations. Section BinaryCoproductFromUnderlying. End BinaryCoproductFromUnderlying.