∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    ∀ {Z : C} (h : X.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.σ j) h)