Lemma iso_between_coproduct_enriched_inv {a b : enriched_coprod_cocone} (Ha : is_coprod_enriched a) (Hb : is_coprod_enriched b) : map_between_coproduct_enriched Ha Hb · map_between_coproduct_enriched Hb Ha = identity _. Proof. unfold map_between_coproduct_enriched. use (is_coprod_enriched_arrow_eq Hb). intro j. rewrite !assoc. rewrite !is_coprod_enriched_arrow_in. rewrite id_right. 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.