Proposition square_to_enriched_nat_trans_enrichment : nat_trans_enrichment square_to_enriched_nat_trans_data EG EF. Proof. use nat_trans_enrichment_via_comp. intros x y. unfold square_to_enriched_nat_trans_data. unfold precomp_arr, postcomp_arr. rewrite !enriched_from_to_arr. rewrite !assoc. rewrite tensor_rinvunitor. rewrite tensor_linvunitor. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_comp_l_id_l. rewrite !assoc'. apply maponpaths. exact (enriched_profunctor_square_rmap_e τ x x y). } cbn. refine (!_). etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_comp_r_id_l. rewrite !assoc'. apply maponpaths. pose (enriched_profunctor_square_lmap_e τ y x y) as p. cbn in p. rewrite !assoc in p. rewrite tensor_sym_mon_braiding in p. pose (maponpaths (λ z, sym_mon_braiding _ _ _ · z) p) as q. cbn in q. rewrite !assoc in q. rewrite !sym_mon_braiding_inv in q. rewrite !id_left in q. exact q. } rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- enrichment_id_left. rewrite <- enrichment_id_right. rewrite mon_linvunitor_lunitor. rewrite mon_rinvunitor_runitor. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.Enriched.Enriched. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.EnrichmentEquiv. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Tensor. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.StandardProfunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.