∀ (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) {m : ℕ}
  (φ : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (i : Fin (m + 1)),
  (X.spine m (X.map φ.op Δ)).vertex i = (X.spine n Δ).vertex ((SimplexCategory.Hom.toOrderHom φ) i)