Definition enriched_profunctor_data_eq_weq {V : sym_mon_closed_cat} (HV : is_univalent V) {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P Q : E₁ ↛e E₂) : pr1 P ╝ pr1 Q ≃ ∑ (f : ∏ (y : C₂) (x : C₁), z_iso (P y x) (Q y x)), (∏ (y₁ y₂ : C₂) (x : C₁), identity _ #⊗ f y₁ x · lmap_e Q y₁ y₂ x = lmap_e P y₁ y₂ x · f y₂ x) × (∏ (y : C₂) (x₁ x₂ : C₁), identity _ #⊗ f y x₁ · rmap_e Q y x₁ x₂ = rmap_e P y x₁ x₂ · f y x₂). Proof. refine (_ ∘ enriched_profunctor_data_eq_weq_help P Q)%weq. use weqbandf. - use weqonsecfibers ; intro y. use weqonsecfibers ; intro x. cbn. exact (make_weq _ (HV _ _)). - intros τ. apply idweq. Defined.
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.Examples.Tensor. 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.EnrichedCats.Profunctors.ProfunctorSquares. 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.