∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X)
  {X_1 Y Z : T} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.comp f g) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk f ⋯) (CategoryTheory.Over.homMk g ⋯)