∀ {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ SimplexCategory.mk (n + 1)),
  ¬Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom θ) →
    ∃ i θ', θ = CategoryTheory.CategoryStruct.comp θ' (SimplexCategory.δ i)