∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_2, u_4} C] {J : Type u_1} [inst_1 : CategoryTheory.SmallCategory J]
  {D : Type u_5} [inst_2 : CategoryTheory.Category.{u_3, u_5} D]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) D]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) D]
  [CategoryTheory.Limits.HasCoequalizers D] (G : CategoryTheory.Functor C D)
  [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) G]
  [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G]
  {K : CategoryTheory.Functor J C},
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C →
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C →
      CategoryTheory.Limits.HasCoequalizers C → CategoryTheory.Limits.PreservesColimit K G