(motive : AugmentedSimplexCategory → AugmentedSimplexCategory → Sort u_1) →
  (m n : AugmentedSimplexCategory) →
    ((m n : SimplexCategory) → motive (CategoryTheory.WithInitial.of m) (CategoryTheory.WithInitial.of n)) →
      ((x : AugmentedSimplexCategory) → motive CategoryTheory.WithInitial.star x) →
        ((x : AugmentedSimplexCategory) → motive x CategoryTheory.WithInitial.star) → motive m n