Definition precomp_enriched_profunctor_data : enriched_profunctor_data E₁ E₂. Proof. use make_enriched_profunctor_data. - exact (λ x y, P (G x) (F y)). - exact (λ x₁ x₂ y, (EG x₂ x₁ #⊗ identity _) · lmap_e P (G x₁) (G x₂) (F y)). - exact (λ x y₁ y₂, (EF y₁ y₂ #⊗ identity _) · rmap_e P (G x) (F y₁) (F y₂)). 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.