Proposition enriched_profunctor_square_rmap_e {V : sym_mon_closed_cat} {C₁ C₂ C₁' C₂' : category} {F : C₁ ⟶ C₁'} {G : C₂ ⟶ C₂'} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {E₁' : enrichment C₁' V} {E₂' : enrichment C₂' V} {EF : functor_enrichment F E₁ E₁'} {EG : functor_enrichment G E₂ E₂'} {P : E₁ ↛e E₂} {Q : E₁' ↛e E₂'} (τ : enriched_profunctor_square EF EG P Q) (x : C₂) (y₁ y₂ : C₁) : EF y₁ y₂ #⊗ τ x y₁ · rmap_e Q (G x) (F y₁) (F y₂) = rmap_e P x y₁ y₂ · τ x y₂. Proof. rewrite tensor_split. rewrite !assoc'. exact (enriched_profunctor_transformation_rmap_e τ x y₁ y₂). 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.EnrichmentTransformation. 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.CurriedBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. 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.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.