{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              (functor : A → CategoryTheory.Functor C D) →
                (shiftIso :
                    (n a a' : A) → n + a = a' → ((functor a').comp (CategoryTheory.shiftFunctor D n) ≅ functor a)) →
                  (∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A)) →
                    (∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
                        shiftIso (m + n) a a'' ⋯ =
                          (functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
                            ((functor a'').associator (CategoryTheory.shiftFunctor D m)
                                  (CategoryTheory.shiftFunctor D n)).symm ≪≫
                              CategoryTheory.Functor.isoWhiskerRight (shiftIso m a' a'' ha'')
                                  (CategoryTheory.shiftFunctor D n) ≪≫
                                shiftIso n a a' ha') →
                      CategoryTheory.SingleFunctors C D A