Proposition square_double_bicat_id_comp_square_laws : double_bicat_id_comp_square_laws square_ver_bicat_sq_id_comp_whisker. Proof. repeat split ; cbn ; intros. - rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite !vassocl. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite rassociator_lassociator. rewrite lwhisker_id2. rewrite id2_left. apply idpath. } etrans. { rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply idpath. } refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite rassociator_rassociator. apply idpath. } etrans. { rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply idpath. } apply maponpaths. refine (!_). etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite lassociator_lassociator. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite lwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite lwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } apply maponpaths. refine (!_). etrans. { rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite <- lassociator_lassociator. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lassociator_rassociator. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply idpath. } apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. rewrite !vassocr. use vcomp_move_R_Mp ; [ is_iso | ] ; cbn. apply lassociator_lassociator. - rewrite lunitor_runitor_identity. rewrite lunitor_V_id_is_left_unit_V_id. apply idpath. - rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite <- lunitor_triangle. rewrite !vassocl. do 2 apply maponpaths. rewrite <- rinvunitor_triangle. rewrite !vassocr. apply maponpaths_2. refine (_ @ id2_left _). apply maponpaths_2. rewrite !vassocl. rewrite lunitor_lwhisker. rewrite rwhisker_vcomp. rewrite rinvunitor_runitor. apply id2_rwhisker. - rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite <- runitor_triangle. rewrite !vassocl. do 2 apply maponpaths. rewrite linvunitor_assoc. rewrite !vassocr. apply maponpaths_2. refine (_ @ id2_left _). apply maponpaths_2. rewrite !vassocl. rewrite runitor_rwhisker. rewrite lwhisker_vcomp. rewrite linvunitor_lunitor. apply lwhisker_id2. 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.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.