Proposition transpose_double_bicat_id_comp_square_laws : double_bicat_id_comp_square_laws transpose_ver_bicat_sq_id_comp_whisker. Proof. repeat split ; intro ; intros ; cbn. - refine (!_). apply double_bicat_interchange. - refine (!_). apply id_h_square_bicat_id. - apply id_v_square_bicat_comp. - apply id_h_square_bicat_comp. 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.