{P : Sort u} →
  {J : CategoryTheory.Limits.MultispanShape} →
    {t : CategoryTheory.Limits.WalkingMultispan J} →
      {J' : CategoryTheory.Limits.MultispanShape} →
        {t' : CategoryTheory.Limits.WalkingMultispan J'} →
          J = J' → t ≍ t' → CategoryTheory.Limits.WalkingMultispan.noConfusionType P t t'