Proposition lmap_e_rmap_e (x₁ x₂ : C₂) (y₁ y₂ : C₁) : sym_mon_braiding V _ _ #⊗ identity _ · mon_lassociator _ _ _ · identity _ #⊗ lmap_e P x₁ x₂ y₁ · rmap_e P x₂ y₁ y₂ = mon_lassociator _ _ _ · identity _ #⊗ rmap_e P x₁ y₁ y₂ · lmap_e P x₁ x₂ y₂. Proof. exact (pr22 (pr222 P) x₁ x₂ y₁ y₂). Defined.
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.