Definition make_is_binary_prod_enriched_from_z_iso (BPV : BinProducts V) (a : enriched_binary_prod_cone) (Ha : ∏ (w : C), is_z_isomorphism (binary_prod_enriched_to_prod BPV a w)) : is_binary_prod_enriched a. Proof. intro w. use (isBinProduct_z_iso (pr2 (BPV (E ⦃ w, x ⦄) (E ⦃ w, y ⦄))) (_ ,, Ha w) _). - abstract (unfold binary_prod_enriched_to_prod ; cbn ; refine (!_) ; apply BinProductPr1Commutes). - abstract (unfold binary_prod_enriched_to_prod ; 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. Import MonoidalNotations. Section BinaryProductFromUnderlying. End BinaryProductFromUnderlying.