Proposition enriched_profunctor_ver_sq_bicat_prebicat_laws : ver_sq_bicat_prebicat_laws enriched_profunctor_ver_sq_bicat_id_comp_cells. Proof. repeat split. - intros C₁ C₂ P Q τ. use eq_enriched_profunctor_transformation ; intros y x ; cbn. apply id_left. - intros C₁ C₂ P Q τ. use eq_enriched_profunctor_transformation ; intros y x ; cbn. apply id_right. - intros C₁ C₂ P₁ P₂ P₃ P₄ τ₁ τ₂ τ₃. use eq_enriched_profunctor_transformation ; intros y x ; cbn. apply assoc. - intros C₁ C₂ C₃ P Q. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intros y. refine (lwhisker_enriched_profunctor_mor_comm _ _ _ _ _ @ _) ; cbn. rewrite tensor_id_id. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ P Q. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intros y. refine (rwhisker_enriched_profunctor_mor_comm _ _ _ _ _ @ _) ; cbn. rewrite tensor_id_id. rewrite id_left, id_right. apply idpath. - intros C₁ C₂ C₃ P Q₁ Q₂ Q₃ τ₁ τ₂. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intros y. rewrite !assoc. etrans. { apply maponpaths_2. apply lwhisker_enriched_profunctor_mor_comm. } rewrite !assoc'. etrans. { apply maponpaths. apply lwhisker_enriched_profunctor_mor_comm. } rewrite !assoc. refine (!_). etrans. { apply lwhisker_enriched_profunctor_mor_comm. } cbn. rewrite <- tensor_comp_id_l. apply idpath. - intros C₁ C₂ C₃ P₁ P₂ P₃ Q τ₁ τ₂. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intro y. rewrite !assoc. etrans. { apply maponpaths_2. apply rwhisker_enriched_profunctor_mor_comm. } rewrite !assoc'. etrans. { apply maponpaths. apply rwhisker_enriched_profunctor_mor_comm. } rewrite !assoc. refine (!_). etrans. { apply rwhisker_enriched_profunctor_mor_comm. } cbn. rewrite <- tensor_comp_id_r. apply idpath. - intros C₁ C₂ P Q τ. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intro y. rewrite !assoc. etrans. { apply maponpaths_2. apply lwhisker_enriched_profunctor_mor_comm. } rewrite !assoc'. etrans. { apply maponpaths. apply lunitor_enriched_profunctor_mor_comm. } refine (enriched_profunctor_transformation_rmap_e _ _ _ _ @ _). refine (!_). rewrite !assoc. apply maponpaths_2. apply lunitor_enriched_profunctor_mor_comm. - intros C₁ C₂ P Q τ. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intro y. rewrite !assoc. etrans. { apply maponpaths_2. apply rwhisker_enriched_profunctor_mor_comm. } rewrite !assoc'. etrans. { apply maponpaths. apply runitor_enriched_profunctor_mor_comm. } rewrite !assoc. rewrite tensor_sym_mon_braiding. rewrite !assoc'. etrans. { apply maponpaths. apply enriched_profunctor_transformation_lmap_e. } refine (!_). rewrite !assoc. apply maponpaths_2. apply runitor_enriched_profunctor_mor_comm. - intros C₁ C₂ C₃ C₄ P Q R₁ R₂ τ. apply enriched_lwhisker_lwhisker. - intros C₁ C₂ C₃ C₄ P Q₁ Q₂ R τ. apply enriched_rwhisker_lwhisker. - intros C₁ C₂ C₃ C₄ P₁ P₂ Q R τ. apply enriched_rwhisker_rwhisker. - intros C₁ C₂ C₃ P₁ P₂ Q₁ Q₂ τ₁ τ₂. use eq_enriched_profunctor_transformation ; intros z x ; cbn. use from_comp_enriched_profunctor_eq. intros y. rewrite !assoc. etrans. { apply maponpaths_2. apply rwhisker_enriched_profunctor_mor_comm. } etrans. { rewrite !assoc'. apply maponpaths. apply lwhisker_enriched_profunctor_mor_comm. } refine (!_). etrans. { apply maponpaths_2. apply lwhisker_enriched_profunctor_mor_comm. } etrans. { rewrite !assoc'. apply maponpaths. apply rwhisker_enriched_profunctor_mor_comm. } rewrite !assoc. rewrite <- tensor_split. rewrite <- tensor_split'. apply idpath. - intros C₁ C₂ P. exact (inv_enriched_profunctor_transformation_right _ (is_iso_lunitor_enriched_profunctor P)). - intros C₁ C₂ P. exact (inv_enriched_profunctor_transformation_left _ (is_iso_lunitor_enriched_profunctor P)). - intros C₁ C₂ P. exact (inv_enriched_profunctor_transformation_right _ (is_iso_runitor_enriched_profunctor P)). - intros C₁ C₂ P. exact (inv_enriched_profunctor_transformation_left _ (is_iso_runitor_enriched_profunctor P)). - intros C₁ C₂ C₃ C₄ P Q R. exact (inv_enriched_profunctor_transformation_right _ (is_iso_lassociator_enriched_profunctor P Q R)). - intros C₁ C₂ C₃ C₄ P Q R. exact (inv_enriched_profunctor_transformation_left _ (is_iso_lassociator_enriched_profunctor P Q R)). - intros C₁ C₂ C₃ P Q. apply enriched_triangle_law. - intros C₁ C₂ C₃ C₄ C₅ P₁ P₂ P₃ P₄. apply enriched_pentagon_law. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. 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.Invertible. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Coend. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.RepresentableLaws. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.EnrichedCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core. Import MonoidalNotations.