English
For a TopCat X and n in SimplexCategoryᵒᵖ, the n-th component of the toSSet object X identifies with the set of continuous maps from the standard simplex to X.
Русский
Для X в TopCat и n в SimplexCategoryᵒᵖ, n-й компонент объекта toSSet X идентифицируется с множеством непрерывных отображений от стандартного простого к X.
LaTeX
$$$$ (toSSet.obj X).obj n \cong \mathrm{C}(n.unop.toTopObj, X) $$$$
Lean4
/-- If `X : TopCat.{u}` and `n : SimplexCategoryᵒᵖ`,
then `(toSSet.obj X).obj n` identifies to the type of continuous
maps from the standard simplex `n.unop.toTopObj` to `X`. -/
def toSSetObjEquiv (X : TopCat.{u}) (n : SimplexCategoryᵒᵖ) : (toSSet.obj X).obj n ≃ C(n.unop.toTopObj, X) :=
Equiv.ulift.{0}.trans (ConcreteCategory.homEquiv.trans (Homeomorph.ulift.continuousMapCongr (.refl _)))
