Definition make_is_coprod_enriched_from_underlying (PV : Products J V) (a : enriched_coprod_cocone) (prod : isCoproduct J C D a (enriched_coprod_cocone_in a)) (HV : conservative_moncat V) : is_coprod_enriched a. Proof. use (make_is_coprod_enriched_from_z_iso PV). intros w. use HV. use isweq_iso. - exact (coprod_from_underlying_arr_map PV a prod w). - exact (coprod_from_underlying_arr_map_eq₁ PV a prod w). - exact (coprod_from_underlying_arr_map_eq₂ PV a prod 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.