{P : Sort u_3} →
  {J : CategoryTheory.Limits.MulticospanShape} →
    {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} →
      {t : I.sections} →
        {J' : CategoryTheory.Limits.MulticospanShape} →
          {I' : CategoryTheory.Limits.MulticospanIndex J' (Type u)} →
            {t' : I'.sections} →
              J = J' → I ≍ I' → t ≍ t' → CategoryTheory.Limits.MulticospanIndex.sections.noConfusionType P t t'