The functor from topological spaces to light condensed sets #
We define the functor topCatToLightCondSet : TopCat.{u} ⥤ LightCondSet.{u}
.
@[reducible, inline]
Associate to a u
-small topological space the corresponding light condensed set, given by
yonedaPresheaf
.
Equations
Instances For
@[reducible, inline]
TopCat.toLightCondSet
yields a functor from TopCat.{u}
to LightCondSet.{u}
.