Proposition enriched_repr_nat_trans_enrichment : nat_trans_enrichment enriched_repr_nat_trans_mor (enriched_repr_presheaf_enrichment y₁) (enriched_repr_presheaf_enrichment y₂). Proof. use nat_trans_enrichment_via_comp. intros x₁ x₂ ; cbn -[sym_mon_braiding]. use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. rewrite self_enrichment_precomp. rewrite internal_beta. rewrite self_enrichment_postcomp. rewrite internal_beta. etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } refine (!_). etrans. { rewrite !assoc. apply maponpaths_2. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } rewrite !assoc'. rewrite enriched_comp_postcomp_arr. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_sym_mon_braiding. rewrite !assoc. rewrite tensor_comp_id_l. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. 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.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations.