Definition iso_between_coproduct_enriched {a b : enriched_coprod_cocone} (Ha : is_coprod_enriched a) (Hb : is_coprod_enriched b) : z_iso a b. Proof. use make_z_iso. - exact (map_between_coproduct_enriched Hb Ha). - exact (map_between_coproduct_enriched Ha Hb). - split. + apply iso_between_coproduct_enriched_inv. + apply iso_between_coproduct_enriched_inv. 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.