∀ {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} {left : X.left ⟶ Y.left} {right : X.right ⟶ Y.right}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map right))
      CategoryTheory.CommaMorphism.w._autoParam}
  {left_1 : X.left ⟶ Y.left} {right_1 : X.right ⟶ Y.right}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left_1) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R.map right_1))
      CategoryTheory.CommaMorphism.w._autoParam},
  { left := left, right := right, w := w } = { left := left_1, right := right_1, w := w_1 } →
    left = left_1 ∧ right = right_1