∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type u_1} [inst_2 : CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) (x : J),
  CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X (K.obj x))