Proposition is_binary_coprod_enriched_arrow_eq {w : C} {f g : a --> w} (q₁ : enriched_coprod_cocone_in1 a · f = enriched_coprod_cocone_in1 a · g) (q₂ : enriched_coprod_cocone_in2 a · f = enriched_coprod_cocone_in2 a · g) : f = g. Proof. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. use (BinProductArrowsEq _ _ _ (is_binary_coprod_enriched_to_BinProduct Ha w)). - cbn. unfold precomp_arr. rewrite !assoc. rewrite !tensor_rinvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split'. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite mon_rinvunitor_I_mon_linvunitor_I. rewrite <- !(enriched_to_arr_comp E). exact q₁. - cbn. unfold precomp_arr. rewrite !assoc. rewrite !tensor_rinvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split'. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite mon_rinvunitor_I_mon_linvunitor_I. rewrite <- !(enriched_to_arr_comp E). exact q₂. 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.