Proposition isaprop_is_binary_prod_enriched (a : enriched_binary_prod_cone) : isaprop (is_binary_prod_enriched a). Proof. use impred ; intro. apply isaprop_isBinProduct. Qed.
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.