∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_2))
  {I : Type u_1} [Small.{u_2, u_1} I] (X : I → C),
  CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun i => P.obj (Opposite.op (X i)))