Proposition lmap_e_lmap_e (x₁ x₂ x₃ : C₂) (y : C₁) : identity _ #⊗ lmap_e P x₁ x₂ y · lmap_e P x₂ x₃ y = mon_rassociator _ _ _ · (sym_mon_braiding V _ _ #⊗ identity _) · enriched_comp E₂ x₃ x₂ x₁ #⊗ identity _ · lmap_e P x₁ x₃ y. Proof. rewrite !assoc'. rewrite lmap_e_comp'. refine (!_). etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_id_r. rewrite sym_mon_braiding_inv. rewrite tensor_id_id. rewrite id_left. apply idpath. } rewrite !assoc. rewrite mon_rassociator_lassociator. rewrite id_left. 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.Enriched.Enriched. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.EnrichmentEquiv. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Tensor. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. 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. Section FromEnrichedProfunctor. End FromEnrichedProfunctor.