Definition transpose_twosided_disp_cat_id_comp : twosided_disp_cat_id_comp transpose_twosided_disp_cat_ob_mor. Proof. simple refine (_ ,, _). - exact (λ (x y : B) (h : x --> y), id_v_square_bicat h). - exact (λ (x₁ y₁ z₁ x₂ y₂ z₂ : B) (hx : x₁ --> x₂) (hy : y₁ --> y₂) (hz : z₁ --> z₂) (v₁ : x₁ -|-> y₁) (v₂ : y₁ -|-> z₁) (w₁ : x₂ -|-> y₂) (w₂ : y₂ -|-> z₂) (s₁ : square_double_bicat hx hy v₁ w₁) (s₂ : square_double_bicat hy hz v₂ w₂), s₁ ⋆v s₂). 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.