Definition enriched_profunctor_laws {V : sym_mon_closed_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P : enriched_profunctor_data E₁ E₂) : UU := (∏ (x : C₂) (y : C₁), enriched_id E₂ x #⊗ identity (P x y) · lmap_e P x x y = mon_lunitor (P x y)) × (∏ (x : C₂) (y : C₁), enriched_id E₁ y #⊗ identity (P x y) · rmap_e P x y y = mon_lunitor (P x y)) × (∏ (x₁ x₂ x₃ : C₂) (y : C₁), (sym_mon_braiding V _ _ · enriched_comp E₂ x₃ x₂ x₁) #⊗ identity _ · lmap_e P x₁ x₃ y = mon_lassociator _ _ _ · identity _ #⊗ lmap_e P x₁ x₂ y · lmap_e P x₂ x₃ y) × (∏ (x : C₂) (y₁ y₂ y₃ : C₁), enriched_comp E₁ y₁ y₂ y₃ #⊗ identity (P x y₁) · rmap_e P x y₁ y₃ = mon_lassociator _ _ _ · identity _ #⊗ rmap_e P x y₁ y₂ · rmap_e P x y₂ y₃) × (∏ (x₁ x₂ : C₂) (y₁ y₂ : C₁), sym_mon_braiding V _ _ #⊗ identity _ · mon_lassociator _ _ _ · identity _ #⊗ lmap_e P x₁ x₂ y₁ · rmap_e P x₂ y₁ y₂ = mon_lassociator _ _ _ · identity _ #⊗ rmap_e P x₁ y₁ y₂ · lmap_e P x₁ 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.Enriched.Enriched. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.EnrichmentEquiv. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Tensor. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. 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. Section FromEnrichedProfunctor. End FromEnrichedProfunctor.