∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (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_1 : A → A → (CategoryTheory.CatCenter C)ˣ)
  (z_zero_zero_1 : autoParam (z_1 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam)
  (assoc_1 :
    autoParam (∀ (a b c : A), z_1 (a + b) c * z_1 a b = z_1 a (b + c) * z_1 b c)
      CategoryTheory.TwistShiftData.assoc._autoParam)
  (commShift_1 :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z_1 a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam),
  ({ z := z, z_zero_zero := z_zero_zero, assoc := assoc, commShift := commShift } =
      { z := z_1, z_zero_zero := z_zero_zero_1, assoc := assoc_1, commShift := commShift_1 }) =
    (z = z_1)