Definition is_prod_enriched_from_iso : is_prod_enriched enriched_prod_cone_from_iso. Proof. intros w. use (isProduct_z_iso _ _ _ _ (Ha w)). - exact (postcomp_arr_z_iso E w (z_iso_inv f)). - abstract (intro j ; cbn ; rewrite <- postcomp_arr_comp ; apply maponpaths ; unfold enriched_prod_cone_from_iso ; cbn ; unfold enriched_prod_cone_pr ; cbn ; rewrite enriched_to_from_arr ; apply idpath). 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.