proposition: Proposition transpose_double_bicat_cylinder_laws : double_bicat_cylinder_laws transpose_ver_bicat_sq_id_comp_whisker.
proof: Proof. repeat split. - intro ; intros ; cbn. refine (!_). apply lassociator_v_comp_square. - intro ; intros ; cbn. refine (!_). apply lassociator_h_comp_square. - intro ; intros ; cbn. refine (!_). apply lunitor_v_comp_square. - intro ; intros ; cbn. refine (!_). apply lunitor_h_comp_square. - intro ; intros ; cbn. refine (!_). apply runitor_v_comp_square. - intro ; intros ; cbn. refine (!_). apply runitor_h_comp_square. - 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. exact (!(hor_bicat_hcomp_h_comp_square B _ _ _ _ _ _ _ _ (!p) (!q))). - 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. exact (!(ver_bicat_hcomp_v_comp_square B _ _ _ _ _ _ _ _ (!p) (!q))). 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.DoubleCategories.DoubleBicat.VerityDoubleBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats