{X : SSet} →
  (spineToSimplex : {n : ℕ} → X.Path n → X.obj (Opposite.op (SimplexCategory.mk n))) →
    (∀ (n : ℕ), X.spine n ∘ spineToSimplex = id) → (∀ (n : ℕ), spineToSimplex ∘ X.spine n = id) → X.StrictSegal