-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
⊢ Eq (α :=
    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
      (op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
            (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
        WalkingParallelPairᵒᵖ)
      (op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
            (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
        WalkingParallelPairᵒᵖ))
    (@WalkingParallelPairHom.casesOn
        (fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : X = a) →
            (h : X = a_1) →
              (h : HEq (α := X ⟶ X) (WalkingParallelPairHom.id X ≫ WalkingParallelPairHom.id X) t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
        X X (WalkingParallelPairHom.id X ≫ WalkingParallelPairHom.id X)
        (fun (h : X = zero) ↦
          Eq.ndrec (motive := fun {X_1 : WalkingParallelPair} ↦
            (f : X_1 ⟶ X) →
              (h : X = one) →
                (h : f ≍ left) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X_1 = t) → WalkingParallelPair) X_1 (fun (h : X_1 = zero) ↦ one)
                          (fun (h : X_1 = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
            (fun (f : zero ⟶ X) (h : X = one) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : zero ⟶ Y) →
                  (h : f ≍ left) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) ⋯ f)
            ⋯ (WalkingParallelPairHom.id X ≫ WalkingParallelPairHom.id X))
        (fun (h : X = zero) ↦
          Eq.ndrec (motive := fun {X_1 : WalkingParallelPair} ↦
            (f : X_1 ⟶ X) →
              (h : X = one) →
                (h : f ≍ right) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X_1 = t) → WalkingParallelPair) X_1 (fun (h : X_1 = zero) ↦ one)
                          (fun (h : X_1 = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
            (fun (f : zero ⟶ X) (h : X = one) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : zero ⟶ Y) →
                  (h : f ≍ right) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) ⋯ f)
            ⋯ (WalkingParallelPairHom.id X ≫ WalkingParallelPairHom.id X))
        (fun (X_1 : WalkingParallelPair) (h : X = X_1) ↦
          Eq.ndrec (motive := fun (X_2 : WalkingParallelPair) ↦
            (h : X = X_2) →
              (h :
                  HEq (α := X ⟶ X) (WalkingParallelPairHom.id X ≫ WalkingParallelPairHom.id X)
                    (WalkingParallelPairHom.id X_2)) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
            (fun (h : X = X) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : X ⟶ Y) →
                  (h : f ≍ WalkingParallelPairHom.id X) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : X ⟶ X) (h : f ≍ WalkingParallelPairHom.id X) ↦
                  Quiver.Hom.op
                    (WalkingParallelPairHom.id
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯)))
                ⋯ (WalkingParallelPairHom.id X ≫ WalkingParallelPairHom.id X))
            h)
        ⋯ ⋯ ⋯ :
      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
              (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
              (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ))
    (CategoryStruct.comp (Y :=
        op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
            (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯))
        (WalkingParallelPairHom.casesOn (motive :=
          fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : X = a) →
            (h : X = a_1) →
              (h : WalkingParallelPairHom.id X ≍ t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
          (WalkingParallelPairHom.id X)
          (fun (h : X = zero) ↦
            Eq.ndrec (motive := fun {X_1 : WalkingParallelPair} ↦
              (f : X_1 ⟶ X) →
                (h : X = one) →
                  (h : f ≍ left) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X_1 = t) → WalkingParallelPair) X_1 (fun (h : X_1 = zero) ↦ one)
                            (fun (h : X_1 = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ X) (h : X = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ left) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) ⋯ f)
              ⋯ (WalkingParallelPairHom.id X))
          (fun (h : X = zero) ↦
            Eq.ndrec (motive := fun {X_1 : WalkingParallelPair} ↦
              (f : X_1 ⟶ X) →
                (h : X = one) →
                  (h : f ≍ right) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X_1 = t) → WalkingParallelPair) X_1 (fun (h : X_1 = zero) ↦ one)
                            (fun (h : X_1 = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ X) (h : X = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ right) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) ⋯ f)
              ⋯ (WalkingParallelPairHom.id X))
          (fun (X_1 : WalkingParallelPair) (h : X = X_1) ↦
            Eq.ndrec (motive := fun (X_2 : WalkingParallelPair) ↦
              (h : X = X_2) →
                (h : WalkingParallelPairHom.id X ≍ WalkingParallelPairHom.id X_2) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
              (fun (h : X = X) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : X ⟶ Y) →
                    (h : f ≍ WalkingParallelPairHom.id X) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : X ⟶ X) (h : f ≍ WalkingParallelPairHom.id X) ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯)))
                  ⋯ (WalkingParallelPairHom.id X))
              h)
          ⋯ ⋯ ⋯)
        (WalkingParallelPairHom.casesOn (motive :=
          fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : X = a) →
            (h : X = a_1) →
              (h : WalkingParallelPairHom.id X ≍ t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
          (WalkingParallelPairHom.id X)
          (fun (h : X = zero) ↦
            Eq.ndrec (motive := fun {X_1 : WalkingParallelPair} ↦
              (f : X_1 ⟶ X) →
                (h : X = one) →
                  (h : f ≍ left) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X_1 = t) → WalkingParallelPair) X_1 (fun (h : X_1 = zero) ↦ one)
                            (fun (h : X_1 = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ X) (h : X = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ left) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) ⋯ f)
              ⋯ (WalkingParallelPairHom.id X))
          (fun (h : X = zero) ↦
            Eq.ndrec (motive := fun {X_1 : WalkingParallelPair} ↦
              (f : X_1 ⟶ X) →
                (h : X = one) →
                  (h : f ≍ right) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X_1 = t) → WalkingParallelPair) X_1 (fun (h : X_1 = zero) ↦ one)
                            (fun (h : X_1 = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ X) (h : X = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ right) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) ⋯ f)
              ⋯ (WalkingParallelPairHom.id X))
          (fun (X_1 : WalkingParallelPair) (h : X = X_1) ↦
            Eq.ndrec (motive := fun (X_2 : WalkingParallelPair) ↦
              (h : X = X_2) →
                (h : WalkingParallelPairHom.id X ≍ WalkingParallelPairHom.id X_2) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
              (fun (h : X = X) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : X ⟶ Y) →
                    (h : f ≍ WalkingParallelPairHom.id X) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : X ⟶ X) (h : f ≍ WalkingParallelPairHom.id X) ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯)))
                  ⋯ (WalkingParallelPairHom.id X))
              h)
          ⋯ ⋯ ⋯) :
      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
              (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
              (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ))

Tactic:
rfl