fact: Definition eq_to_pb_obj {a b₁ b₂ b₃ : B} {f : b₁ --> b₃} {g : b₂ --> b₃} {h₁ h₂ : a --> f /≃ g} {φ ψ : h₁ ==> h₂} {p : cell_to_pb_obj_homot (φ ▹ π₁) (φ ▹ π₂)} (φψpr1 : φ ▹ π₁ = ψ ▹ π₁) (φψpr2 : φ ▹ π₂ = ψ ▹ π₂) : φ = ψ := pb_ump_eq (pr2 (pr2 B _ _ _ f g)) h₁ h₂ (φ ▹ π₁) (φ ▹ π₂) p φ ψ (idpath _) (idpath _) (!φψpr1) (!φψpr2).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Limits.Pullbacks