Definition representable_enriched_profunctor_left_data : enriched_profunctor_data E₁ E₂. Proof. use make_enriched_profunctor_data. - exact (λ x y, E₂ ⦃ x , F y ⦄). - exact (λ x₁ x₂ y, sym_mon_braiding V _ _ · enriched_comp E₂ _ _ _). - exact (λ x y₁ y₂, (EF y₁ y₂ #⊗ identity _) · enriched_comp E₂ _ _ _). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.