Properties of morphisms in the simplex category

In this file, we show that morphisms in the simplex category are generated by faces and degeneracies. This is stated by saying that if W : MorphismProperty SimplexCategory is multiplicative, and contains faces and degeneracies, then W = ⊤. This statement is deduced from a similar statement for the category SimplexCategory.Truncated d.

theorem SimplexCategory.Truncated.morphismProperty_eq_top {d : ℕ} (W : CategoryTheory.MorphismProperty (Truncated d)) [W.IsMultiplicative] (δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)) (σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)) : W = ⊤

theorem SimplexCategory.morphismProperty_eq_top (W : CategoryTheory.MorphismProperty SimplexCategory) [W.IsMultiplicative] (δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)) (σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)) : W = ⊤