proposition: Proposition square_whisker_square_bicat_law : whisker_square_bicat_law square_ver_bicat_sq_id_comp_whisker.
proof: Proof. repeat split ; cbn ; intros. - rewrite id2_rwhisker. rewrite id2_right. apply idpath. - rewrite <- rwhisker_vcomp. rewrite !vassocl. apply idpath. - rewrite lwhisker_id2. rewrite id2_left. apply idpath. - rewrite <- lwhisker_vcomp. rewrite !vassocl. apply idpath. - rewrite id2_rwhisker. rewrite id2_left. apply idpath. - rewrite <- rwhisker_vcomp. rewrite !vassocl. apply idpath. - rewrite lwhisker_id2. rewrite id2_right. apply idpath. - rewrite <- lwhisker_vcomp. rewrite !vassocl. apply idpath. - rewrite !vassocl. apply idpath. - rewrite !vassocl. apply idpath. - rewrite !vassocr. rewrite vcomp_whisker. apply idpath. - rewrite !vassocl. rewrite vcomp_whisker. apply idpath. - rewrite !vassocl. apply idpath. - rewrite !vassocl. apply idpath. - rewrite !vassocr. rewrite vcomp_lunitor. rewrite !vassocl. apply maponpaths. rewrite rinvunitor_natural. rewrite rwhisker_hcomp. apply idpath. - rewrite !vassocr. rewrite vcomp_runitor. rewrite !vassocl. apply maponpaths. rewrite linvunitor_natural. rewrite lwhisker_hcomp. apply idpath. - rewrite !vassocr. do 2 apply maponpaths_2. rewrite <- rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. rewrite <- rwhisker_vcomp. rewrite !vassocr. apply idpath. - rewrite !vassocl. do 3 apply maponpaths. rewrite <- lwhisker_lwhisker. rewrite !vassocr. rewrite <- lwhisker_vcomp. apply idpath. - apply maponpaths_2. rewrite !vassocl. apply maponpaths. rewrite <- rwhisker_vcomp. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker_rassociator. rewrite !vassocl. rewrite lwhisker_vcomp. apply idpath. - rewrite !vassocl. do 3 apply maponpaths. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocr. rewrite rwhisker_vcomp. apply idpath. - rewrite !vassocr. do 3 apply maponpaths_2. rewrite <- lwhisker_lwhisker_rassociator. rewrite !vassocl. rewrite lwhisker_vcomp. apply idpath. - apply maponpaths_2. rewrite !vassocl. apply maponpaths. rewrite <- lwhisker_vcomp. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. rewrite rwhisker_vcomp. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.AdjointUnique UniMath.Bicategories.DoubleCategories.DoubleBicat.Core