fact: Definition eq_comma_1cell {p q : comma_cone} (φ ψ : comma_1cell p q) (r₁ : pr1 φ = pr1 ψ) (r₂ : pr1 (comma_1cell_pr1 φ) = (idtoiso_2_1 _ _ r₁ ▹ comma_cone_pr1 q) • pr1 (comma_1cell_pr1 ψ)) (r₃ : pr1 (comma_1cell_pr2 φ) = (idtoiso_2_1 _ _ r₁ ▹ comma_cone_pr2 q) • pr1 (comma_1cell_pr2 ψ)) : φ = ψ.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence