English
Let X be the (n+1)-truncated simplicial set with a strict Segal structure. For every m there exists a natural equivalence between the m-simplices of X (at level n+1) and the space of paths in X of length m, given by the spine map and its inverse provided by the strict Segal data.
Русский
Пусть X — n+1-ограниченное симпликсальное множество с жесткой сегаловой структурой. Для каждого целого m существует естественное эквивалентное отображение между m-гранями X на уровне n+1 и пространством путей Path(X, m), заданное отображением позвоночника и его обратной связью, задаваемой структурой StrictSegal.
LaTeX
$$$X_{\langle m\rangle} \simeq Path(X,m)$$$
Lean4
/-- The fields of `StrictSegal` define an equivalence between `X _⦋m⦌ₙ₊₁`
and `Path X m`. -/
def spineEquiv : (X _⦋m⦌ₙ ₊ ₁) ≃ Path X m where
toFun := X.spine m
invFun := sx.spineToSimplex m h
left_inv := sx.spineToSimplex_spine_apply m h
right_inv := sx.spine_spineToSimplex_apply m h
