Definition transpose_twosided_disp_cat_id_comp : twosided_disp_cat_id_comp transpose_twosided_disp_cat_ob_mor. Proof. split. - exact (λ x y f, id_h_square f). - refine (λ x₁ x₂ x₃ y₁ y₂ y₃ h₁ h₂ h₃ vx₁ vx₂ vy₁ vy₂ s₁ s₂, _). cbn in s₁, s₂ ; cbn. exact (s₁ ⋆h s₂). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Comma. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws. Import TransportSquare.