∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (F : CategoryTheory.Functor C (Type u_1))
  {X Y Z : F.Elements} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.StructuredArrow.homMk ↑(CategoryTheory.CategoryStruct.comp f g) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.homMk ↑f ⋯)
      (CategoryTheory.StructuredArrow.homMk ↑g ⋯)