Proposition is_binary_coprod_enriched_arrow_in2 {w : C} (f : x --> w) (g : y --> w) : enriched_coprod_cocone_in2 a · is_binary_coprod_enriched_arrow f g = g. Proof. unfold is_binary_coprod_enriched_arrow, enriched_coprod_cocone_in2. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn. refine (_ @ BinProductPr2Commutes _ _ _ (is_binary_coprod_enriched_to_BinProduct Ha w) _ (enriched_from_arr E f) (enriched_from_arr E g)). cbn. unfold precomp_arr, enriched_coprod_cocone_in2. rewrite enriched_from_arr_comp. rewrite !assoc. apply maponpaths_2. rewrite !enriched_from_to_arr. rewrite tensor_rinvunitor. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite !assoc'. apply maponpaths. rewrite <- tensor_split'. apply idpath. Qed.
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.