Definition comp_h_enriched_profunctor_square_data {V : sym_mon_closed_cat} {C₁ C₂ C₃ C₁' C₂' C₃' : category} {F₁ : C₁ ⟶ C₂} {F₂ : C₂ ⟶ C₃} {G₁ : C₁' ⟶ C₂'} {G₂ : C₂' ⟶ C₃'} {EC₁ : enrichment C₁ V} {EC₂ : enrichment C₂ V} {EC₃ : enrichment C₃ V} {EC₁' : enrichment C₁' V} {EC₂' : enrichment C₂' V} {EC₃' : enrichment C₃' V} {EF₁ : functor_enrichment F₁ EC₁ EC₂} {EF₂ : functor_enrichment F₂ EC₂ EC₃} {EG₁ : functor_enrichment G₁ EC₁' EC₂'} {EG₂ : functor_enrichment G₂ EC₂' EC₃'} {P₁ : EC₁ ↛e EC₁'} {P₂ : EC₂ ↛e EC₂'} {P₃ : EC₃ ↛e EC₃'} (τ : enriched_profunctor_square EF₁ EG₁ P₁ P₂) (θ : enriched_profunctor_square EF₂ EG₂ P₂ P₃) : enriched_profunctor_transformation_data P₁ (precomp_enriched_profunctor (functor_comp_enrichment EF₁ EF₂) (functor_comp_enrichment EG₁ EG₂) P₃) := λ x y, τ x 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.