proposition: Proposition isaprop_enrichment_binary_prod {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) : isaprop (enrichment_binary_prod E).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use funextsec ; intro x. use funextsec ; intro y. use subtypePath. { intro. apply isaprop_is_binary_prod_enriched. } use total2_paths_f. - use (isotoid _ HC). use iso_between_product_enriched. + exact (pr2 (φ₁ x y)). + exact (pr2 (φ₂ x y)). - rewrite transportf_dirprod. use pathsdirprod. + 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. apply is_binary_prod_enriched_arrow_pr1. + 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. apply is_binary_prod_enriched_arrow_pr2. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.Limits.BinProducts