Definition make_is_prod_enriched_from_z_iso (PV : Products J V) (a : enriched_prod_cone) (Ha : ∏ (w : C), is_z_isomorphism (prod_enriched_to_prod PV a w)) : is_prod_enriched a. Proof. intro w. use (isProduct_z_iso _ _ _ _ (pr2 (PV (λ j, E ⦃ w , D j ⦄)))). - exact (z_iso_inv (_ ,, Ha w)). - abstract (intro j ; unfold prod_enriched_to_prod ; cbn ; refine (!_) ; apply (ProductPrCommutes _ _ _ (PV (λ j, E ⦃ w , D j ⦄)))). 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.