fact: Definition make_comma_1cell {p q : comma_cone} (φ : p --> q) (τ : invertible_2cell (φ · comma_cone_pr1 q) (comma_cone_pr1 p)) (θ : invertible_2cell (φ · comma_cone_pr2 q) (comma_cone_pr2 p)) (H : φ ◃ comma_cone_cell q = lassociator _ _ _ • (τ ▹ f) • comma_cone_cell p • (θ^-1 ▹ g) • rassociator _ _ _) : comma_1cell p q := (φ ,, τ ,, θ ,, H).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence