Definition eq_pb_1cell {p q : pb_cone} (φ ψ : pb_1cell p q) (r₁ : pr1 φ = pr1 ψ) (r₂ : pr1 (pb_1cell_pr1 φ) = (idtoiso_2_1 _ _ r₁ ▹ pb_cone_pr1 q) • pr1 (pb_1cell_pr1 ψ)) (r₃ : pr1 (pb_1cell_pr2 φ) = (idtoiso_2_1 _ _ r₁ ▹ pb_cone_pr2 q) • pr1 (pb_1cell_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.