∀ {T : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} T] {J : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : (CategoryTheory.Functor.const J).obj X ⟶ D) {X_1 Y Z : J} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Under.homMk (D.map (CategoryTheory.CategoryStruct.comp f g)) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.homMk (D.map f) ⋯) (CategoryTheory.Under.homMk (D.map g) ⋯)