Definition make_is_binary_coprod_enriched_from_z_iso (BPV : BinProducts V) (a : enriched_binary_coprod_cocone) (Ha : ∏ (w : C), is_z_isomorphism (binary_coprod_enriched_to_coprod BPV a w)) : is_binary_coprod_enriched a. Proof. intro w. use (isBinProduct_z_iso (pr2 (BPV (E ⦃ x , w ⦄) (E ⦃ y , w ⦄))) (_ ,, Ha w) _). - abstract (unfold binary_coprod_enriched_to_coprod ; cbn ; refine (!_) ; apply BinProductPr1Commutes). - abstract (unfold binary_coprod_enriched_to_coprod ; cbn ; refine (!_) ; apply BinProductPr2Commutes). 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Import MonoidalNotations. Section BinaryCoproductFromUnderlying. End BinaryCoproductFromUnderlying.