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