{P : Sort u} →
  {J : Type v} →
    {inst : CategoryTheory.SmallCategory J} →
      {F : CategoryTheory.Functor J CommRingCat} →
        {t : CommRingCat.Colimits.Prequotient F} →
          {J' : Type v} →
            {inst' : CategoryTheory.SmallCategory J'} →
              {F' : CategoryTheory.Functor J' CommRingCat} →
                {t' : CommRingCat.Colimits.Prequotient F'} →
                  J = J' → inst ≍ inst' → F ≍ F' → t ≍ t' → CommRingCat.Colimits.Prequotient.noConfusionType P t t'