Proposition isaprop_enrichment_prod {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) (J : UU) : isaprop (enrichment_prod E J). Proof. use invproofirrelevance. intros φ₁ φ₂. use funextsec ; intro D. use subtypePath. { intro. apply isaprop_is_prod_enriched. } use total2_paths_f. - use (isotoid _ HC). use iso_between_product_enriched. + exact (pr2 (φ₁ D)). + exact (pr2 (φ₂ D)). - rewrite transportf_sec_constant. use funextsec. intro j. rewrite transportf_enriched_arr_l. rewrite idtoiso_inv. rewrite idtoiso_isotoid. cbn. refine (_ @ enriched_from_to_arr E _). apply maponpaths. unfold map_between_product_enriched ; cbn. etrans. { apply is_prod_enriched_arrow_pr. } apply idpath. 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.Products. Import MonoidalNotations. Section ProductFromUnderlying. End ProductFromUnderlying.