Proposition eq_profunctor_quantale_enrichment {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P Q : E₁ ↛e E₂) (p : ∏ (y : C₂) (x : C₁), P y x = Q y x) : P = Q. Proof. use subtypePath. { intro. apply isaprop_enriched_profunctor_laws. } use subtypePath. { intro. use isapropdirprod ; repeat (use impred ; intro) ; apply (isaprop_mor_quantale_enrichment_univalent_cat (self_enrichment V)). } use funextsec ; intro y. use funextsec ; intro x. exact (p y x). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.PosetCat. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Import MonoidalNotations.