∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : G ⟶ F)
  {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).map f).f = f.f