(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] →
                CategoryTheory.Category.{v_1, u_1} (CategoryTheory.PullbackShift C φ)