Proposition mate_ver_sq_bicat_prebicat_laws : ver_sq_bicat_prebicat_laws mate_ver_sq_bicat_id_comp_cells. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.