Definition enriched_profunctor_univalent_cat {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₂) : P = Q ≃ ∑ (τ : enriched_profunctor_transformation P Q), is_iso_enriched_profunctor_transformation τ. Proof. refine (_ ∘ path_sigma_hprop _ _ _ _)%weq. { apply isaprop_enriched_profunctor_laws. } refine (_ ∘ total2_paths_equiv _ _ _)%weq. refine (_ ∘ enriched_profunctor_data_eq_weq HV P Q)%weq. apply enriched_profunctor_univalent_cat_help. 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.