Lean4
/-- The functor associating the *singular simplicial set* to a topological space.
Let `X : TopCat.{u}` be a topological space.
Then the singular simplicial set of `X`
has as `n`-simplices the continuous maps `ULift.{u} ⦋n⦌.toTop → X`.
Here, `⦋n⦌.toTop` is the standard topological `n`-simplex,
defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology. -/
noncomputable def toSSet : TopCat.{u} ⥤ SSet.{u} :=
Presheaf.restrictedULiftYoneda.{0} SimplexCategory.toTop.{u}