∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (q : Quotient (CommRingCat.Colimits.colimitSetoid F)), Quotient.map CommRingCat.Colimits.Prequotient.neg ⋯ q + q = 0