∀ {A : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} A] {B : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_3, u_5} B] {T : Type u_6} [inst_2 : CategoryTheory.Category.{u_4, u_6} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (P : CategoryTheory.MorphismProperty T)
  (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B)
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W}, X = Y → X.left = Y.left