∀ {T : Type u_6} [inst : CategoryTheory.Category.{u_4, u_6} T] {D : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_3, u_5} D] {C : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} C]
  (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C)
  {X Y : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      { left := CategoryTheory.Under.mk X.hom, right := X.right.right, hom := X.right.hom }.left.hom f.right.left =
    { left := CategoryTheory.Under.mk Y.hom, right := Y.right.right, hom := Y.right.hom }.left.hom