Definition map_between_coproduct_enriched {a b : enriched_binary_coprod_cocone} (Ha : is_binary_coprod_enriched a) (Hb : is_binary_coprod_enriched b) : a --> b := is_binary_coprod_enriched_arrow Ha (enriched_coprod_cocone_in1 b) (enriched_coprod_cocone_in2 b).
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.