Proposition lunitor_enriched_profunctor_mor_eq (y : C₂) (x x' x'' : C₁) : (sym_mon_braiding _ _ _ · enriched_comp E₁ x' x'' x) #⊗ identity _ · rmap_e P y x' x = sym_mon_braiding _ _ _ #⊗ identity _ · mon_lassociator _ _ _ · identity _ #⊗ rmap_e P y x' x'' · rmap_e P y x'' x. Proof. rewrite tensor_comp_id_r. rewrite !assoc'. apply maponpaths. rewrite rmap_e_comp. rewrite !assoc. 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.StandardProfunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Invertible. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.CompositionProf. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.