∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C]
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C]
  [CategoryTheory.Limits.HasEqualizers C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G],
  CategoryTheory.Limits.PreservesLimitsOfShape J G