∀ {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} {W X Y Z : CategoryTheory.Comma L R}
  (f : CategoryTheory.CommaMorphism W X) (g : CategoryTheory.CommaMorphism X Y) (h : CategoryTheory.CommaMorphism Y Z),
  {
      left :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.comp f.left g.left,
              right := CategoryTheory.CategoryStruct.comp f.right g.right, w := ⋯ }.left
          h.left,
      right :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.comp f.left g.left,
              right := CategoryTheory.CategoryStruct.comp f.right g.right, w := ⋯ }.right
          h.right,
      w := ⋯ } =
    {
      left :=
        CategoryTheory.CategoryStruct.comp f.left
          { left := CategoryTheory.CategoryStruct.comp g.left h.left,
              right := CategoryTheory.CategoryStruct.comp g.right h.right, w := ⋯ }.left,
      right :=
        CategoryTheory.CategoryStruct.comp f.right
          { left := CategoryTheory.CategoryStruct.comp g.left h.left,
              right := CategoryTheory.CategoryStruct.comp g.right h.right, w := ⋯ }.right,
      w := ⋯ }