Definition make_is_binary_prod_enriched_from_underlying (BPV : BinProducts V) (a : enriched_binary_prod_cone) (prod : isBinProduct C x y a (enriched_prod_cone_pr1 a) (enriched_prod_cone_pr2 a)) (HV : conservative_moncat V) : is_binary_prod_enriched a. Proof. use (make_is_binary_prod_enriched_from_z_iso BPV). intros w. use HV. use isweq_iso. - exact (prod_from_underlying_arr_map BPV a prod w). - exact (prod_from_underlying_arr_map_eq₁ BPV a prod w). - exact (prod_from_underlying_arr_map_eq₂ BPV a prod w). 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.