Definition make_is_coprod_enriched_from_z_iso (PV : Products J V) (a : enriched_coprod_cocone) (Ha : ∏ (w : C), is_z_isomorphism (coprod_enriched_to_prod PV a w)) : is_coprod_enriched a. Proof. intro w. use (isProduct_z_iso _ _ _ _ (pr2 (PV (λ j, E ⦃ D j , w ⦄)))). - exact (z_iso_inv (_ ,, Ha w)). - abstract (intro j ; unfold coprod_enriched_to_prod ; cbn ; refine (!_) ; apply (ProductPrCommutes _ _ _ (PV (λ j, E ⦃ D j , 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.Products. Require Import UniMath.CategoryTheory.Limits.Coproducts. Import MonoidalNotations. Section CoproductFromUnderlying. End CoproductFromUnderlying.