Definition transpose_ver_sq_bicat_id_comp_cells : ver_sq_bicat_id_comp_cells transpose_ver_sq_bicat_ver_id_comp. Proof. repeat split ; cbn. - intros. apply id2. - intros. apply lunitor. - intros. apply runitor. - intros. apply linvunitor. - intros. apply rinvunitor. - intros. apply rassociator. - intros. apply lassociator. - exact (λ _ _ _ _ _ τ θ, τ • θ). - exact (λ _ _ _ f _ _ τ, f ◃ τ). - exact (λ _ _ _ _ _ f τ, τ ▹ f). Defined.
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.