Definition make_quantale_enriched_profunctor_data {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P : C₂ → C₁ → V) (Pl : ∏ (x₁ x₂ : C₂) (y : C₁), E₂ ⦃ x₂, x₁ ⦄ ⊗ P x₁ y --> P x₂ y) (Pr : ∏ (x : C₂) (y₁ y₂ : C₁), E₁ ⦃ y₁, y₂ ⦄ ⊗ P x y₁ --> P x y₂) : enriched_profunctor_data E₁ E₂. Proof. use make_enriched_profunctor_data. - exact P. - exact Pl. - exact Pr. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.PosetCat. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. 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.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Import MonoidalNotations.