Proposition transpose_double_bicat_cylinder_laws : double_bicat_cylinder_laws transpose_ver_bicat_sq_id_comp_whisker. 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.
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.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats.