Definition pb_ump_eq (τ₁ τ₂ : φ ==> ψ) (τ₁_pr1 : τ₁ ▹ pb_cone_pr1 p = α) (τ₁_pr2 : τ₁ ▹ pb_cone_pr2 p = β) (τ₂_pr1 : τ₂ ▹ pb_cone_pr1 p = α) (τ₂_pr2 : τ₂ ▹ pb_cone_pr2 p = β) : τ₁ = τ₂ := maponpaths pr1 (proofirrelevance _ (isapropifcontr (pr2 Hp q φ ψ α β r)) (τ₁ ,, τ₁_pr1 ,, τ₁_pr2) (τ₂ ,, τ₂_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.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence.