{J : Type u_1} →
  (motive :
      (x x_1 x_2 : CategoryTheory.Limits.WalkingParallelFamily J) →
        CategoryTheory.Limits.WalkingParallelFamily.Hom J x x_1 →
          CategoryTheory.Limits.WalkingParallelFamily.Hom J x_1 x_2 → Sort u_2) →
    (x x_1 x_2 : CategoryTheory.Limits.WalkingParallelFamily J) →
      (x_3 : CategoryTheory.Limits.WalkingParallelFamily.Hom J x x_1) →
        (x_4 : CategoryTheory.Limits.WalkingParallelFamily.Hom J x_1 x_2) →
          ((x x_5 : CategoryTheory.Limits.WalkingParallelFamily J) →
              (h : CategoryTheory.Limits.WalkingParallelFamily.Hom J x x_5) →
                motive x x x_5 (CategoryTheory.Limits.WalkingParallelFamily.Hom.id x) h) →
            ((j : J) →
                motive CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one
                  CategoryTheory.Limits.WalkingParallelFamily.one
                  (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
                  (CategoryTheory.Limits.WalkingParallelFamily.Hom.id
                    CategoryTheory.Limits.WalkingParallelFamily.one)) →
              motive x x_1 x_2 x_3 x_4