Proposition enriched_functor_hom_from_arr_eq (x y : C₁) : enriched_from_arr E₂ (τ x) · enriched_functor_left_map_ob EG x y = enriched_from_arr E₂ (τ y) · enriched_functor_right_map_ob EF x y. Proof. pose (p := Eτ x y). use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. unfold enriched_functor_left_map_ob, enriched_functor_right_map_ob. rewrite !assoc'. rewrite !internal_beta. rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !assoc'. etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply tensor_split'. } rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split. apply idpath. } etrans. { rewrite !assoc. rewrite <- tensor_sym_mon_braiding. rewrite !assoc'. do 2 apply maponpaths. refine (!(id_left _) @ _). rewrite <- mon_runitor_rinvunitor. rewrite !assoc'. apply maponpaths. rewrite !assoc. exact p. } clear p. rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { apply maponpaths_2. apply tensor_split. } rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite sym_mon_braiding_runitor. rewrite mon_lunitor_linvunitor. rewrite id_left. rewrite <- tensor_split'. 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.