Proposition coprod_from_underlying_arr_map_eq₂ (f : I_{V} --> PV (λ j, E ⦃ D j , w ⦄)) : coprod_from_underlying_arr_map f · coprod_enriched_to_prod PV a w = f. Proof. unfold coprod_from_underlying_arr_map. use (ProductArrow_eq _ _ _ (PV (λ j, E ⦃ D j , w ⦄))). unfold coprod_enriched_to_prod. intro j. rewrite !assoc'. etrans. { apply maponpaths. apply (ProductPrCommutes _ _ _ (PV (λ k, E ⦃ D k , w ⦄)) _ _ j). } rewrite enriched_from_arr_precomp. refine (_ @ enriched_from_to_arr E _). apply maponpaths. apply (CoproductInCommutes _ _ _ (make_Coproduct _ _ _ _ _ coprod)). 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.