∀ (C : Type u_1) {A : Type u_3} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A),
  a = 0 → CategoryTheory.shiftFunctor C a = CategoryTheory.shiftFunctor C 0