Proposition enriched_profunctor_transformation_to_whiskered_laws {V : sym_mon_closed_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {P Q : E₁ ↛e E₂} (τ : enriched_profunctor_transformation P Q) : whiskered_enriched_transformation_laws (enriched_profunctor_transformation_to_whiskered_data τ). Proof. split. - intros x₁ x₂ y ; cbn in *. rewrite self_enrichment_precomp, self_enrichment_postcomp. use internal_funext. intros z h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. rewrite !internal_beta. etrans. { rewrite tensor_split. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite internal_beta. apply idpath. } refine (!_). etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. rewrite tensor_comp_id_l. apply idpath. } rewrite !assoc'. apply maponpaths. clear z h. apply enriched_profunctor_transformation_lmap_e. - intros x y₁ y₂ ; cbn in *. rewrite self_enrichment_precomp, self_enrichment_postcomp. use internal_funext. intros z h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. rewrite !internal_beta. etrans. { rewrite tensor_split. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite internal_beta. apply idpath. } refine (!_). etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. rewrite tensor_comp_id_l. apply idpath. } rewrite !assoc'. apply maponpaths. clear z h. apply enriched_profunctor_transformation_rmap_e. Qed.
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.