Proposition curried_enriched_transformation_to_whiskered_laws {V : sym_monoidal_cat} {C₁ C₂ C₃ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {E₃ : enrichment C₃ V} {F G : enriched_whiskered_bifunctor E₁ E₂ E₃} (τ : curried_enriched_transformation (enriched_whiskered_bifunctor_to_curried F) (enriched_whiskered_bifunctor_to_curried G)) : whiskered_enriched_transformation_laws (curried_enriched_transformation_to_whiskered_data τ). Proof. split. - intros x₁ x₂ y ; cbn. pose (maponpaths (λ z, mon_rinvunitor _ · identity _ #⊗ enriched_id _ _ · z) (curried_enriched_transformation_natural τ x₁ x₂ y y)) as p. refine (_ @ p @ _) ; cbn ; clear p. + rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. rewrite !enriched_whiskered_bifunctor_right_id. rewrite tensor_split'. rewrite !assoc'. rewrite <- enrichment_id_right. rewrite tensor_runitor. apply idpath. } rewrite !assoc. rewrite mon_rinvunitor_runitor. apply id_left. + rewrite !assoc. apply maponpaths_2. etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. rewrite !enriched_whiskered_bifunctor_right_id. rewrite tensor_split'. rewrite !assoc'. rewrite <- enrichment_id_right. rewrite tensor_runitor. apply idpath. } rewrite !assoc. rewrite mon_rinvunitor_runitor. apply id_left. - intros x y₁ y₂ ; cbn. pose (maponpaths (λ z, mon_linvunitor _ · enriched_id _ _ #⊗ identity _ · z) (curried_enriched_transformation_natural τ x x y₁ y₂)) as p. refine (_ @ p @ _) ; cbn ; clear p. + rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. rewrite !enriched_whiskered_bifunctor_left_id. rewrite tensor_split. rewrite !assoc'. rewrite <- enrichment_id_left. rewrite tensor_lunitor. apply idpath. } rewrite !assoc. rewrite mon_linvunitor_lunitor. apply id_left. + rewrite !assoc. apply maponpaths_2. etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_left. rewrite !enriched_whiskered_bifunctor_left_id. rewrite tensor_split. rewrite !assoc'. rewrite <- enrichment_id_left. rewrite tensor_lunitor. apply idpath. } rewrite !assoc. rewrite mon_linvunitor_lunitor. apply id_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. 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.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import MonoidalNotations.