Proposition is_coprod_enriched_arrow_in {w : C} (f : ∏ (j : J), D j --> w) (j : J) : enriched_coprod_cocone_in a j · is_coprod_enriched_arrow f = f j. Proof. unfold is_coprod_enriched_arrow, enriched_coprod_cocone_in. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn. refine (_ @ ProductPrCommutes _ _ _ (is_coprod_enriched_to_Product Ha w) _ (λ j, enriched_from_arr E (f j)) j). cbn. unfold precomp_arr, enriched_coprod_cocone_in. rewrite enriched_from_arr_comp. rewrite !assoc. apply maponpaths_2. rewrite tensor_rinvunitor. rewrite !assoc'. rewrite mon_linvunitor_I_mon_rinvunitor_I. apply maponpaths. rewrite <- tensor_split'. rewrite !enriched_from_to_arr. 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.Products. Require Import UniMath.CategoryTheory.Limits.Coproducts. Import MonoidalNotations. Section CoproductFromUnderlying. End CoproductFromUnderlying.