{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {A : Type w} →
      {inst_1 : AddMonoid A} →
        {inst_2 : CategoryTheory.HasShift C A} →
          {P : Sort u_1} →
            {z : A → A → (CategoryTheory.CatCenter C)ˣ} →
              {z_zero_zero : autoParam (z 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam} →
                {assoc :
                    autoParam (∀ (a b c : A), z (a + b) c * z a b = z a (b + c) * z b c)
                      CategoryTheory.TwistShiftData.assoc._autoParam} →
                  {commShift :
                      autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z a b)) A)
                        CategoryTheory.TwistShiftData.commShift._autoParam} →
                    {z' : A → A → (CategoryTheory.CatCenter C)ˣ} →
                      {z_zero_zero' : autoParam (z' 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam} →
                        {assoc' :
                            autoParam (∀ (a b c : A), z' (a + b) c * z' a b = z' a (b + c) * z' b c)
                              CategoryTheory.TwistShiftData.assoc._autoParam} →
                          {commShift' :
                              autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z' a b)) A)
                                CategoryTheory.TwistShiftData.commShift._autoParam} →
                            { z := z, z_zero_zero := z_zero_zero, assoc := assoc, commShift := commShift } =
                                { z := z', z_zero_zero := z_zero_zero', assoc := assoc', commShift := commShift' } →
                              (z ≍ z' → P) → P