Definition make_is_prod_enriched (a : enriched_prod_cone) (pair : ∏ (w : C) (v : V) (f : ∏ (j : J), v --> E ⦃ w , D j ⦄), v --> E ⦃ w , a ⦄) (pair_pr : ∏ (w : C) (v : V) (f : ∏ (j : J), v --> E ⦃ w , D j ⦄) (j : J), pair w v f · postcomp_arr E w (enriched_prod_cone_pr a j) = f j) (pair_eq : ∏ (w : C) (v : V) (φ₁ φ₂ : v --> E ⦃ w , a ⦄) (q : ∏ (j : J), φ₁ · postcomp_arr E w (enriched_prod_cone_pr a j) = φ₂ · postcomp_arr E w (enriched_prod_cone_pr a j)), φ₁ = φ₂) : is_prod_enriched a. Proof. intro w. use make_isProduct. { apply homset_property. } intros v f. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; use impred ; intro ; apply homset_property | ] ; exact (pair_eq w v (pr1 φ₁) (pr1 φ₂) (λ j, pr2 φ₁ j @ !(pr2 φ₂ j)))). - simple refine (_ ,, _). + exact (pair w v f). + exact (pair_pr w v f). 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.Products. Import MonoidalNotations. Section ProductFromUnderlying. End ProductFromUnderlying.