Definition comma_ump_2 : UU := ∏ (q : B) (φ ψ : q --> p) (α : φ · comma_cone_pr1 p ==> ψ · comma_cone_pr1 p) (β : φ · comma_cone_pr2 p ==> ψ · comma_cone_pr2 p) (r : (φ ◃ comma_cone_cell p) • lassociator _ _ _ • (β ▹ g) • rassociator _ _ _ = lassociator _ _ _ • (α ▹ f) • rassociator _ _ _ • (ψ ◃ comma_cone_cell p)), ∃! (γ : φ ==> ψ), (γ ▹ comma_cone_pr1 p = α) × (γ ▹ comma_cone_pr2 p = β).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence.