Proposition comp_enriched_profunctor_rmap_e_arr {x₁ x₂ : C₁} (f : x₁ --> x₂) (y : C₂) (z : C₃) : comp_enriched_profunctor_in z x₁ y · rmap_e_arr comp_enriched_profunctor f z = (rmap_e_arr P f y #⊗ identity _) · comp_enriched_profunctor_in z x₂ y. Proof. etrans. { unfold rmap_e_arr ; cbn. rewrite !assoc. rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_split'. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_l. rewrite tensor_sym_mon_braiding. rewrite !assoc'. rewrite comp_enriched_profunctor_rmap_comm. rewrite !assoc. rewrite sym_mon_braiding_inv. apply id_left. } unfold comp_enriched_profunctor_rmap_mor. rewrite !assoc. apply maponpaths_2. unfold rmap_e_arr. rewrite !tensor_comp_id_r. apply maponpaths_2. rewrite <- tensor_id_id. rewrite !assoc'. rewrite tensor_rassociator. rewrite !assoc. apply maponpaths_2. rewrite <- mon_linvunitor_triangle. rewrite !assoc'. rewrite mon_lassociator_rassociator. apply id_right. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Coends. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Coend. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.