Definition enrichment_data_hom_path_help {C : precategory_data} {V : monoidal_cat} (E₁ E₂ : enrichment_data C V) : UU := ∑ (fs : ∏ (x y : C), z_iso (pr1 E₁ x y) (pr1 E₂ x y)), (∏ (x : C), enriched_id E₁ x · fs x x = enriched_id E₂ x) × (∏ (x y z : C), enriched_comp E₁ x y z · fs x z = fs y z #⊗ fs x y · enriched_comp E₂ x y z) × (∏ (x y : C) (f : x --> y), enriched_from_arr E₁ f · fs x y = enriched_from_arr E₂ f) × (∏ (x y : C) (f : I_{V} --> E₁ ⦃ x , y ⦄), enriched_to_arr E₁ f = enriched_to_arr E₂ (f · fs x y)).
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.covyoneda. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.