Proposition enrichment_functor_hom_to_arr_enrichment : nat_trans_enrichment enrichment_functor_hom_to_arr_data EF EG. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations. Section EnrichmentFromArr. End EnrichmentFromArr.