∀ {n : ℕ} {Δ : SimplexCategory} (f : SimplexCategory.mk n ⟶ Δ) (i₁ i₂ : Fin ((SimplexCategory.mk (n + 1)).len + 1)),
  i₁ ≤ i₂ →
    SSet.Augmented.StandardSimplex.shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤
      SSet.Augmented.StandardSimplex.shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂