Definition pb_2cell_on_comp {a₁ a₂ b₁ b₂ : B} (f : b₁ --> b₂) {g₁ : a₁ --> b₂} {g₂ : a₂ --> b₂} {h₁ h₂ h₃ : a₁ --> a₂} {α : invertible_2cell g₁ (h₁ · g₂)} {β : invertible_2cell g₁ (h₂ · g₂)} {γ : invertible_2cell g₁ (h₃ · g₂)} (δ₁ : h₁ ==> h₂) (p : α • (δ₁ ▹ g₂) = β) (δ₂ : h₂ ==> h₃) (q : β • (δ₂ ▹ g₂) = γ) (r : α • ((δ₁ • δ₂) ▹ g₂) = γ) : f /≃₂ r = f /≃₂ p • f /≃₂ q.
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.