Definition is_binary_coprod_enriched_from_iso : is_binary_coprod_enriched enriched_binary_prod_cone_from_iso. Proof. intros w. use (isBinProduct_z_iso (Ha w)). - exact (precomp_arr_z_iso E w f). - abstract (cbn ; rewrite <- precomp_arr_comp ; apply maponpaths ; unfold enriched_binary_prod_cone_from_iso ; cbn ; unfold enriched_coprod_cocone_in1 ; cbn ; rewrite enriched_to_from_arr ; apply idpath). - abstract (cbn ; rewrite <- precomp_arr_comp ; apply maponpaths ; unfold enriched_binary_prod_cone_from_iso ; cbn ; unfold enriched_coprod_cocone_in2 ; cbn ; rewrite enriched_to_from_arr ; apply idpath). 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.