∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : Type u_1} [inst_1 : CategoryTheory.SmallCategory J]
  {K : CategoryTheory.Functor J C},
  CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C →
    CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C →
      CategoryTheory.Limits.HasEqualizers C → CategoryTheory.Limits.HasLimit K