fact: Definition comma_1cell_pr2 {p q : comma_cone} (φ : comma_1cell p q) : invertible_2cell (φ · comma_cone_pr2 q) (comma_cone_pr2 p) := pr122 φ.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence