Proposition comp_enriched_profunctor_lmap_e_arr (x : C₁) (y : C₂) {z₁ z₂ : C₃} (g : z₁ --> z₂) : comp_enriched_profunctor_in _ x y · lmap_e_arr comp_enriched_profunctor x g = (identity _ #⊗ lmap_e_arr Q y g) · comp_enriched_profunctor_in z₁ x y. Proof. etrans. { unfold lmap_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_lmap_comm. rewrite !assoc. rewrite sym_mon_braiding_inv. apply id_left. } unfold comp_enriched_profunctor_lmap_mor. rewrite !assoc. apply maponpaths_2. unfold lmap_e_arr. rewrite !tensor_comp_id_l. rewrite !assoc. apply maponpaths_2. etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_id_id. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite <- tensor_comp_id_l. rewrite tensor_sym_mon_braiding. rewrite tensor_comp_id_l. apply idpath. } rewrite !assoc. apply maponpaths_2. rewrite sym_mon_braiding_linvunitor. rewrite <- mon_rinvunitor_triangle. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite mon_rassociator_lassociator. apply id_left. } rewrite <- tensor_comp_id_l. rewrite sym_mon_braiding_rinvunitor. apply idpath. 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.