The category of topological spaces notoriously lacks some desirable features. There are therefore quite a few attempts to define “big” categories that contain (all) interesting topological spaces but are better behaved categorically. The topological topos was proposed in this vein by Peter Johnstone in the seventies. As it is conceptually based on sequential convergence it plays an important role in constructive mathematics.
Let Top be the category of topological spaces, and let be the full subcategory whose only two objects are a one-point space and , the one-point compactification of the discrete space of natural numbers. Let be the canonical Grothendieck topology on .
The category of subsequential spaces can also be found as a full subcategory of this topos (in fact, it consists of the separated objects for a Lawvere-Tierney topology). A general object of the topos can be thought of as being like a subsequential space, but such that a given sequence can converge to a given point in “more than one way.”
Importantly, following an idea by Joyal, the topological topos allows one to represent the geometric realization functor as the inverse image of a geometric morphism from to the topos of simplicial sets. As Johnstone points out, this approach fails for the big topos on and also for Lawvere’s topos for continuum mechanics.
The topological topos was introduced in
Peter Johnstone, Topos Theory , Academic Press New York 1977. (Dover reprint 2014; exercise 0.10, p.21)
An example of a type-theoretic universe in the topological topos is studied in
Generalizations of the construction of the topological topos occur in the following two papers:
R. Montañez, Topoi generated by topological spaces , Talk CT15 Aveiro 2015. (pdf-slides)
C. Ruiz, R. Montañez, Elevadores de Estructura , Boletín de Matemáticas XIII no.2 (2006) pp.111–135. (link)