{P : Sort u} →
  {J : Type w} →
    {a a_1 : CategoryTheory.Limits.WalkingParallelFamily J} →
      {t : CategoryTheory.Limits.WalkingParallelFamily.Hom J a a_1} →
        {J' : Type w} →
          {a' a'_1 : CategoryTheory.Limits.WalkingParallelFamily J'} →
            {t' : CategoryTheory.Limits.WalkingParallelFamily.Hom J' a' a'_1} →
              J = J' →
                a ≍ a' → a_1 ≍ a'_1 → t ≍ t' → CategoryTheory.Limits.WalkingParallelFamily.Hom.noConfusionType P t t'