Definition binary_prod_enriched_to_prod (BPV : BinProducts V) (a : enriched_binary_prod_cone) (w : C) : E ⦃ w, a ⦄ --> BPV (E ⦃ w, x ⦄) (E ⦃ w, y ⦄). Proof. use BinProductArrow. - exact (postcomp_arr E w (enriched_prod_cone_pr1 a)). - exact (postcomp_arr E w (enriched_prod_cone_pr2 a)). 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.