proposition: Proposition profunctor_associator_laws : double_associator_laws profunctor_associator_data.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Categories.CategoryOfSetCategories UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Categories.HSET.SetCoends UniMath.CategoryTheory.Profunctors.Core UniMath.CategoryTheory.Profunctors.Examples UniMath.CategoryTheory.Profunctors.Squares UniMath.CategoryTheory.Profunctors.Transformation UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProfunctorTwosidedDispCat UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints