{J : Type v} →
  {inst : CategoryTheory.SmallCategory J} →
    {F : CategoryTheory.Functor J RingCat} →
      {P : Sort u} → {a a' : RingCat.Colimits.Prequotient F} → a.neg = a'.neg → (a ≍ a' → P) → P