fact: Definition comma_ump_mor_pr2 (q : comma_cone) : invertible_2cell (comma_ump_mor q · comma_cone_pr2 p) (comma_cone_pr2 q) := comma_1cell_pr2 (pr1 Hp q).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence