∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (F : CategoryTheory.Functor C C)
  {X Y Z : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f