Proposition profunctor_associator_laws : double_associator_laws profunctor_associator_data. Proof. intros C₁ C₂ C₃ C₄ C₅ C₆ C₇ C₈ P₁ P₂ Q₁ Q₂ R₁ R₂ F₁ F₂ F₃ F₄ τ₁ τ₂ τ₃ ; cbn in *. use eq_profunctor_square. intros x₁ x₂ h. etrans. { apply transportf_disp_mor2_profunctors. } use mor_from_comp_profunctor_ob_eq ; clear h. intros x₃ h k. use (mor_from_comp_profunctor_ob_eq Q₁ R₁ x₁ x₃ (λ k, comp_h_profunctor_square (associator_profunctor_square P₁ Q₁ R₁) (comp_v_profunctor_square (comp_v_profunctor_square τ₁ τ₂) τ₃) x₁ x₂ (comp_profunctor_ob_in P₁ (comp_profunctor Q₁ R₁) x₃ h k)) (λ k, comp_h_profunctor_square (comp_v_profunctor_square τ₁ (comp_v_profunctor_square τ₂ τ₃)) (associator_profunctor_square P₂ Q₂ R₂) x₁ x₂ (comp_profunctor_ob_in P₁ (comp_profunctor Q₁ R₁) x₃ h k))). clear k. intros y k l ; cbn. rewrite associator_profunctor_nat_trans_mor_comm. etrans. { apply maponpaths. apply associator_profunctor_nat_trans_mor_ob_comm. } etrans. { apply (comp_v_profunctor_square_mor_comm (comp_v_profunctor_square τ₁ τ₂) τ₃). } cbn. etrans. { apply maponpaths_2. apply (comp_v_profunctor_square_mor_comm τ₁ τ₂). } refine (!_). etrans. { apply maponpaths. apply (comp_v_profunctor_square_mor_comm τ₁ (comp_v_profunctor_square τ₂ τ₃)). } rewrite associator_profunctor_nat_trans_mor_comm. cbn. etrans. { apply maponpaths. apply (comp_v_profunctor_square_mor_comm τ₂ τ₃). } etrans. { exact (associator_profunctor_nat_trans_mor_ob_comm P₂ Q₂ R₂ (τ₁ x₃ x₂ h) (τ₂ y x₃ k) (τ₃ x₁ y l)). } apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares. Require Import UniMath.CategoryTheory.Profunctors.Transformation. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProfunctorTwosidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints.