∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] (φ : A →+ B) [inst_3 : CategoryTheory.HasShift C B] {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  (F : CategoryTheory.Functor C D), CategoryTheory.PullbackShift.functor φ F = F