proposition: Proposition enrichment_functor_hom_to_arr_enrichment : nat_trans_enrichment enrichment_functor_hom_to_arr_data EF EG.
proof: Proof. unfold enrichment_functor_hom_to_arr_data. intros x y ; cbn. rewrite !enriched_from_to_arr. rewrite tensor_comp_r_id_l. rewrite tensor_comp_l_id_l. pose (enriched_functor_hom_eq' EF EG x y) as p. rewrite !assoc'. rewrite <- p. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite tensor_sym_mon_braiding. rewrite !assoc. apply maponpaths_2. rewrite sym_mon_braiding_linvunitor. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products