Proposition mate_whisker_square_bicat_law : whisker_square_bicat_law mate_ver_bicat_sq_id_comp_whisker. Proof. repeat split ; intros ; cbn. - 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.
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.