proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products