Proposition enriched_functor_hom_id_eq (x y : C₁) : enriched_id E₂ (F x) · enriched_functor_left_map_ob EF x y = enriched_id E₂ (F y) · enriched_functor_right_map_ob EF x y. Proof. 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. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split'. rewrite !assoc'. rewrite <- enrichment_id_right. apply idpath. } refine (!_). etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite <- enrichment_id_left. apply idpath. } rewrite tensor_lunitor. rewrite tensor_runitor. rewrite !assoc. do 2 apply maponpaths_2. rewrite sym_mon_braiding_runitor. 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.