Definition enriched_profunctor_univalent_cat_help {V : sym_mon_closed_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P Q : E₁ ↛e E₂) : (∑ (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₂)) ≃ ∑ (τ : enriched_profunctor_transformation P Q), is_iso_enriched_profunctor_transformation τ. Proof. use weq_iso. - intros τ. simple refine (_ ,, _). + use make_enriched_profunctor_transformation. * exact (λ y x, pr1 τ y x). * exact (pr2 τ). + intros y x. apply z_iso_is_z_isomorphism. - intro τ. simple refine (_ ,, _ ,, _). + refine (λ y x, pr1 τ y x ,, _). apply (pr2 τ). + intros. apply enriched_profunctor_transformation_lmap_e. + intros y x₁ x₂. apply enriched_profunctor_transformation_rmap_e. - abstract (intro ; apply idpath). - abstract (intro ; apply idpath). 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.