English
The type of simplices of X is naturally equivalent to the type X.Elements, i.e., there is a canonical bijection between simplices and elements viewed as a functor.
Русский
Тип симплекс X естественным образом эквивалентен типу X.Elements, т.е. существует каноническое биективное соответствие между симплексами и элементами, рассматриваемыми как функтор.
LaTeX
$$$X.S \simeq X.Elements$$$
Lean4
/-- The type of simplices of `X : SSet.{u}` identifies to the type
of elements of `X` considered as a functor `SimplexCategoryᵒᵖ ⥤ Type u`.
(Note that this is not an (anti)equivalence of categories,
see `S.le_iff_nonempty_hom`.) -/
@[simps!]
def equivElements : X.S ≃ X.Elements where
toFun s := X.elementsMk _ s.simplex
invFun := by
rintro ⟨⟨n⟩, x⟩
induction n using SimplexCategory.rec
exact S.mk x
left_inv _ := rfl
right_inv _ := rfl
