proposition: Proposition square_ver_sq_bicat_prebicat_laws : ver_sq_bicat_prebicat_laws square_ver_sq_bicat_id_comp_cells.
proof: Proof. repeat split ; cbn ; intros. - apply id2_right. - apply id2_left. - apply vassocl. - apply lwhisker_id2. - apply id2_rwhisker. - apply lwhisker_vcomp. - apply rwhisker_vcomp. - rewrite lwhisker_hcomp. rewrite <- linvunitor_natural. apply idpath. - rewrite rwhisker_hcomp. rewrite <- rinvunitor_natural. apply idpath. - apply lwhisker_lwhisker_rassociator. - apply rwhisker_lwhisker_rassociator. - apply rwhisker_rwhisker_alt. - refine (!_). apply vcomp_whisker. - apply lunitor_linvunitor. - apply linvunitor_lunitor. - apply runitor_rinvunitor. - apply rinvunitor_runitor. - apply lassociator_rassociator. - apply rassociator_lassociator. - rewrite rwhisker_hcomp, lwhisker_hcomp. rewrite triangle_r_inv. apply idpath. - rewrite !vassocr. rewrite rassociator_rassociator. 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