Definition iso_between_product_enriched {a b : enriched_binary_prod_cone} (Ha : is_binary_prod_enriched a) (Hb : is_binary_prod_enriched b) : z_iso a b. Proof. use make_z_iso. - exact (map_between_product_enriched Ha Hb). - exact (map_between_product_enriched Hb Ha). - split. + apply iso_between_product_enriched_inv. + apply iso_between_product_enriched_inv. 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.BinProducts. Import MonoidalNotations. Section BinaryProductFromUnderlying. End BinaryProductFromUnderlying.