Definition uwhisker_enriched_profunctor_square_data {V : sym_mon_closed_cat} {C₁ C₂ C₁' C₂' : category} {EC₁ : enrichment C₁ V} {EC₂ : enrichment C₂ V} {EC₁' : enrichment C₁' V} {EC₂' : enrichment C₂' V} {F F' : C₁ ⟶ C₂} {τ : F ⟹ F'} {EF : functor_enrichment F EC₁ EC₂} {EF' : functor_enrichment F' EC₁ EC₂} {G : C₁' ⟶ C₂'} {EG : functor_enrichment G EC₁' EC₂'} {P : EC₁ ↛e EC₁'} {Q : EC₂ ↛e EC₂'} (Eτ : nat_trans_enrichment τ EF EF') (θ : enriched_profunctor_square EF EG P Q) : enriched_profunctor_transformation_data P (precomp_enriched_profunctor EF' EG Q) := λ x y, θ x y · mon_linvunitor _ · (enriched_from_arr EC₂ (τ y) #⊗ identity _) · rmap_e Q (G x) (F y) (F' y).
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.