Proposition square_double_bicat_cylinder_laws : double_bicat_cylinder_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. etrans. { rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite lwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite rassociator_lassociator. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocl. apply idpath. } apply maponpaths. 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 maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. use vcomp_move_R_Mp ; [ is_iso | ] ; cbn. refine (!_). apply rassociator_rassociator. - intros. rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite !vassocl. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite lassociator_lassociator. rewrite !vassocl. apply idpath. } apply maponpaths. 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. etrans. { rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ] ; cbn. etrans. { rewrite !vassocr. rewrite lassociator_lassociator. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. use vcomp_move_R_Mp ; [ is_iso | ] ; cbn. refine (!_). apply lassociator_lassociator. - intros. rewrite <- !rwhisker_vcomp. rewrite !vassocl. rewrite lunitor_lwhisker. rewrite rwhisker_vcomp. rewrite rinvunitor_runitor. rewrite id2_rwhisker. rewrite id2_right. rewrite lunitor_triangle. rewrite vcomp_lunitor. rewrite !vassocr. apply maponpaths_2. rewrite <- lunitor_triangle. rewrite !vassocr. rewrite rassociator_lassociator. apply id2_left. - intros. rewrite <- !rwhisker_vcomp. rewrite !vassocl. refine (!_). etrans. { rewrite !vassocr. rewrite lwhisker_hcomp. rewrite triangle_l_inv. rewrite <- rwhisker_hcomp. rewrite rwhisker_vcomp. rewrite rinvunitor_runitor. rewrite id2_rwhisker. rewrite id2_left. rewrite <- linvunitor_assoc. rewrite lwhisker_hcomp. rewrite <- linvunitor_natural. rewrite !vassocl. apply idpath. } apply maponpaths. rewrite linvunitor_assoc. rewrite !vassocl. rewrite rassociator_lassociator. apply id2_right. - intros. rewrite <- !lwhisker_vcomp. rewrite !vassocl. rewrite runitor_triangle. rewrite vcomp_runitor. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- runitor_triangle. etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. apply id2_left. } rewrite lwhisker_vcomp. rewrite rinvunitor_runitor. rewrite lwhisker_id2. rewrite id2_right. rewrite lunitor_lwhisker. apply idpath. - intros. rewrite <- !lwhisker_vcomp. rewrite !vassocl. refine (!_). etrans. { do 5 apply maponpaths. rewrite lwhisker_hcomp. rewrite triangle_l_inv. rewrite <- rwhisker_hcomp. apply idpath. } rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite runitor_triangle. rewrite vcomp_runitor. refine (_ @ id2_left _). rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- runitor_triangle. etrans. { apply maponpaths. rewrite !vassocr. rewrite lassociator_rassociator. apply id2_left. } rewrite lwhisker_vcomp. rewrite rinvunitor_runitor. rewrite lwhisker_id2. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ h₁ h₂ h₃ v₁ v₁' v₂ v₂'. intros w₁ w₁' w₂ w₂' τ₁ τ₂ θ₁ θ₂ s₁ s₁' s₂ s₂' p q. rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite !vassocl. refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite <- p. rewrite <- rwhisker_vcomp. rewrite !vassocl. apply idpath. } clear p. etrans. { rewrite !vassocr. rewrite lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply idpath. } do 2 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } rewrite <- rwhisker_rwhisker. rewrite !vassocr. apply maponpaths_2. rewrite <- lwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite <- q ; clear q. rewrite <- lwhisker_vcomp. rewrite !vassocl. apply maponpaths. rewrite rwhisker_lwhisker. apply idpath. - intros x₁ x₂ y₁ y₂ z₁ z₂ h₁ h₂ h₃ v₁ v₁' v₂ v₂'. intros w₁ w₁' w₂ w₂' τ₁ τ₂ θ₁ θ₂ s₁ s₁' s₂ s₂' p q. unfold hcomp. rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp. rewrite !vassocl. etrans. { do 3 apply maponpaths. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite rwhisker_lwhisker_rassociator. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite p. rewrite <- rwhisker_vcomp. apply idpath. } clear p. rewrite !vassocl. rewrite lwhisker_lwhisker_rassociator. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite vcomp_whisker. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite vcomp_whisker. etrans. { apply maponpaths. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- lwhisker_lwhisker. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite q. rewrite <- lwhisker_vcomp. apply idpath. } clear q. rewrite !vassocl. rewrite rwhisker_rwhisker. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- vcomp_whisker. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- vcomp_whisker. rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite rwhisker_lwhisker_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.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.