∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.IsFinitelyPresentable X ↔
    CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1}
      (CategoryTheory.coyoneda.obj (Opposite.op X))