Proposition bicat_to_associator_laws : double_associator_laws bicat_to_associator_data. Proof. intros w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ f₁ f₂ g₁ g₂ h₁ h₂ p₁ p₂ p₃ p₄ s₁ s₂ s₃. induction p₁, p₂, p₃, p₄ ; cbn. rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite linvunitor_lunitor. rewrite id2_left. rewrite !vassocl. apply maponpaths. apply idpath. } refine (!_). etrans. { do 10 apply maponpaths. rewrite !vassocr. rewrite rinvunitor_runitor. rewrite id2_left. apply idpath. } etrans. { rewrite !vassocr. do 10 apply maponpaths_2. rewrite lwhisker_hcomp. rewrite <- inverse_pentagon_3. rewrite <- rwhisker_hcomp. apply idpath. } etrans. { rewrite !vassocr. do 9 apply maponpaths_2. rewrite !vassocl. rewrite lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocl. refine (!_). etrans. { rewrite !vassocr. do 8 apply maponpaths_2. rewrite !vassocl. rewrite <- rinvunitor_triangle. rewrite !vassocl. rewrite lassociator_rassociator. rewrite id2_right. rewrite !vassocr. rewrite <- vcomp_runitor. rewrite !vassocl. apply maponpaths. rewrite <- runitor_triangle. rewrite !vassocl. rewrite lwhisker_vcomp. rewrite runitor_rinvunitor. rewrite lwhisker_id2. apply id2_right. } rewrite !vassocl. do 3 apply maponpaths. rewrite !vassocr. rewrite inverse_pentagon_7. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite pentagon_6. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite <- vcomp_lunitor. rewrite !vassocl. rewrite lunitor_linvunitor. apply id2_right. } rewrite !vassocr. rewrite inverse_pentagon_7. rewrite !vassocl. rewrite lassociator_rassociator. rewrite id2_right. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats.