∀ (motive : (X Y : CategoryTheory.Limits.WalkingParallelPair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingParallelPair) → motive x x (CategoryTheory.Limits.WalkingParallelPairHom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one
        CategoryTheory.Limits.WalkingParallelPairHom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one
        CategoryTheory.Limits.WalkingParallelPairHom.right),
  (match CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.WalkingParallelPair.one,
      CategoryTheory.Limits.WalkingParallelPairHom.right with
    | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one),
      CategoryTheory.Limits.WalkingParallelPairHom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one),
      CategoryTheory.Limits.WalkingParallelPairHom.right => h_3 ()) =
    h_3 ()