proposition: Proposition vertical_two_cat_category_idto2mor {x y : C} {f g : x -->v y} (p : f = g) : idto2mor (C := strict_underlying_vertical_two_cat_data) p = transportf_s_square (idpath _) p (idpath _) (idpath _) (s_id_h_square f).
proof: Proof. induction p ; cbn. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.TwoCategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics UniMath.Bicategories.DoubleCategories.Core.StrictDoubleCats