(motive : AugmentedSimplexCategory → AugmentedSimplexCategory → AugmentedSimplexCategory → Sort u_1) →
  (x y z : AugmentedSimplexCategory) →
    ((x y z : SimplexCategory) →
        motive (CategoryTheory.WithInitial.of x) (CategoryTheory.WithInitial.of y) (CategoryTheory.WithInitial.of z)) →
      (Unit → motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star) →
        ((a : SimplexCategory) →
            motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) CategoryTheory.WithInitial.star) →
          ((a : SimplexCategory) →
              motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star
                (CategoryTheory.WithInitial.of a)) →
            ((a a_1 : SimplexCategory) →
                motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a)
                  (CategoryTheory.WithInitial.of a_1)) →
              ((a : SimplexCategory) →
                  motive (CategoryTheory.WithInitial.of a) CategoryTheory.WithInitial.star
                    CategoryTheory.WithInitial.star) →
                ((a a_1 : SimplexCategory) →
                    motive (CategoryTheory.WithInitial.of a) CategoryTheory.WithInitial.star
                      (CategoryTheory.WithInitial.of a_1)) →
                  ((a a_1 : SimplexCategory) →
                      motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1)
                        CategoryTheory.WithInitial.star) →
                    motive x y z