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).
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.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Limits.Pullbacks.