Proposition is_binary_prod_enriched_arrow_eq {w : C} {f g : w --> a} (q₁ : f · enriched_prod_cone_pr1 a = g · enriched_prod_cone_pr1 a) (q₂ : f · enriched_prod_cone_pr2 a = g · enriched_prod_cone_pr2 a) : f = g. Proof. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. use (BinProductArrowsEq _ _ _ (is_binary_prod_enriched_to_BinProduct Ha w)). - cbn. unfold postcomp_arr. rewrite !assoc. rewrite !tensor_linvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite <- !(enriched_to_arr_comp E). exact q₁. - cbn. unfold postcomp_arr. rewrite !assoc. rewrite !tensor_linvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite <- !(enriched_to_arr_comp E). exact q₂. 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.