{J : Type v} →
  {inst : CategoryTheory.Category.{u, v} J} →
    {F : CategoryTheory.Functor J MonCat} →
      {P : Sort u_1} →
        {a a_1 a' a'_1 : MonCat.Colimits.Prequotient F} → a.mul a_1 = a'.mul a'_1 → (a ≍ a' → a_1 ≍ a'_1 → P) → P