∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (F : CategoryTheory.Functor C C)
  (X : CategoryTheory.Endofunctor.Coalgebra F),
  (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.V