Definition whiskered_enriched_profunctor_transformation_weq {V : sym_mon_closed_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P Q : E₁ ↛e E₂) : whiskered_enriched_transformation (enriched_profunctor_to_whiskered P) (enriched_profunctor_to_whiskered Q) ≃ enriched_profunctor_transformation P Q. Proof. use weq_iso. - exact whiskered_to_enriched_profunctor_transformation. - exact enriched_profunctor_transformation_to_whiskered. - abstract (intro τ ; use eq_whiskered_enriched_transformation ; intros ; apply idpath). - abstract (intro τ ; use eq_enriched_profunctor_transformation ; intros ; 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.Enriched.Enriched. Require Import UniMath.CategoryTheory.EnrichedCats.Enriched.EnrichmentEquiv. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Tensor. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. 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.