∀ {A : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {x y : CategoryTheory.Comma L R},
  x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.hom ≍ y.hom