Proposition enriched_whiskered_bifunctor_to_profunctor_laws : enriched_profunctor_laws enriched_whiskered_bifunctor_to_profunctor_data. Proof. repeat split. - intros x y ; cbn. rewrite !assoc. rewrite <- tensor_comp_id_r. etrans. { do 2 apply maponpaths_2. exact (enriched_whiskered_bifunctor_left_id P x y). } cbn. unfold internal_id. rewrite internal_beta. apply idpath. - intros x y ; cbn. rewrite !assoc. rewrite <- tensor_comp_id_r. etrans. { do 2 apply maponpaths_2. exact (enriched_whiskered_bifunctor_right_id P x y). } cbn. unfold internal_id. rewrite internal_beta. apply idpath. - intros x₁ x₂ x₃ y ; cbn. rewrite !assoc. rewrite <- !tensor_comp_id_r. etrans. { do 2 apply maponpaths_2. exact (enriched_whiskered_bifunctor_left_comp P x₁ x₂ x₃ y). } cbn. rewrite tensor_comp_id_r. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. rewrite !assoc. rewrite tensor_lassociator. apply maponpaths_2. rewrite !assoc'. apply maponpaths. rewrite <- !tensor_comp_mor. rewrite !id_left, !id_right. apply idpath. - intros x₁ x₂ x₃ y ; cbn. rewrite !assoc. rewrite <- !tensor_comp_id_r. etrans. { do 2 apply maponpaths_2. exact (enriched_whiskered_bifunctor_right_comp P x₁ x₂ x₃ y). } cbn. rewrite tensor_comp_id_r. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. rewrite !assoc. rewrite tensor_lassociator. apply maponpaths_2. rewrite !assoc'. apply maponpaths. rewrite <- !tensor_comp_mor. rewrite !id_left, !id_right. apply idpath. - intros x₁ x₂ y₁ y₂ ; cbn. pose (maponpaths (λ z, z #⊗ identity _ · internal_eval _ _) (enriched_whiskered_bifunctor_left_right P x₁ x₂ y₁ y₂)) as p. cbn in p. rewrite !tensor_comp_r_id_r in p. rewrite !assoc' in p. unfold internal_comp in p. rewrite !internal_beta in p. rewrite !assoc in p. rewrite tensor_lassociator in p. rewrite !assoc'. refine (!_). etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split. apply idpath. } etrans. { rewrite !assoc. refine (_ @ p). apply maponpaths_2. rewrite !assoc'. apply maponpaths. rewrite <- tensor_comp_mor. rewrite id_right. apply idpath. } clear p. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. apply maponpaths_2. rewrite !assoc'. apply maponpaths. rewrite <- !tensor_comp_mor. rewrite !id_right, id_left. apply idpath. 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.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. 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. Section FromEnrichedProfunctor. End FromEnrichedProfunctor.