proposition: Proposition id_h_square_bicat_id (x : B) : id_h_square_bicat (id_v x) = id_v_square_bicat (id_h x).
proof: Proof. exact (pr1 (pr2 (pr122 B)) x). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat