{C : Type u} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        {motive : CategoryTheory.HasShift C A → Sort u_1} →
          (t : CategoryTheory.HasShift C A) →
            ((shift : CategoryTheory.Functor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)) →
                (shiftMonoidal : shift.Monoidal) → motive { shift := shift, shiftMonoidal := shiftMonoidal }) →
              motive t