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

Tactic:
cases g