∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsCofiltered C ↔
    ∀ {J : Type v} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C),
      ∃ X, Nonempty (CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))))