The functor from topological spaces to light condensed sets

We define the functor topCatToLightCondSet : TopCat.{u} ⥤ LightCondSet.{u}.

@[reducible, inline]

noncomputable abbrev TopCat.toLightCondSet (X : TopCat) : LightCondSet

Associate to a u-small topological space the corresponding light condensed set, given by yonedaPresheaf.

@[reducible, inline]

noncomputable abbrev topCatToLightCondSet : CategoryTheory.Functor TopCat LightCondSet

TopCat.toLightCondSet yields a functor from TopCat.{u} to LightCondSet.{u}.