Lemma iso_between_coproduct_enriched_inv {a b : enriched_binary_coprod_cocone} (Ha : is_binary_coprod_enriched a) (Hb : is_binary_coprod_enriched b) : map_between_coproduct_enriched Ha Hb · map_between_coproduct_enriched Hb Ha = identity _. Proof. unfold map_between_coproduct_enriched. use (is_binary_coprod_enriched_arrow_eq Ha). - rewrite !assoc. rewrite !is_binary_coprod_enriched_arrow_in1. rewrite id_right. apply idpath. - rewrite !assoc. rewrite !is_binary_coprod_enriched_arrow_in2. 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Import MonoidalNotations. Section BinaryCoproductFromUnderlying. End BinaryCoproductFromUnderlying.