∀ {A : Type u_4} [inst : CategoryTheory.Category.{u_1, u_4} A] {B : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_2, u_5} B] {T : Type u_6} [inst_2 : CategoryTheory.Category.{u_3, u_6} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R}
  (f : CategoryTheory.CommaMorphism X Y),
  {
      left :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.id X.left, right := CategoryTheory.CategoryStruct.id X.right,
              w := ⋯ }.left
          f.left,
      right :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.id X.left, right := CategoryTheory.CategoryStruct.id X.right,
              w := ⋯ }.right
          f.right,
      w := ⋯ } =
    f