Lemma iso_between_product_enriched_inv {a b : enriched_binary_prod_cone} (Ha : is_binary_prod_enriched a) (Hb : is_binary_prod_enriched b) : map_between_product_enriched Ha Hb · map_between_product_enriched Hb Ha = identity _. Proof. unfold map_between_product_enriched. use (is_binary_prod_enriched_arrow_eq Ha). - rewrite !assoc'. rewrite !is_binary_prod_enriched_arrow_pr1. rewrite id_left. apply idpath. - rewrite !assoc'. rewrite !is_binary_prod_enriched_arrow_pr2. rewrite id_left. 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.BinProducts. Import MonoidalNotations. Section BinaryProductFromUnderlying. End BinaryProductFromUnderlying.