The category $Top$ 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 $\Sigma$ be the full subcategory whose only two objects are a one-point space and $\mathbb{N}^+$, the one-point compactification of the discrete space of natural numbers. Let $J$ be the canonical Grothendieck topology on $\Sigma$.
Johnstone’s topological topos (specifically, the one described in the eponymous paper) is the topos of canonical sheaves $Sh_J(\Sigma)$ on $\Sigma$. The functor
is faithful and factors through $Sh_J(\Sigma)$, and its restriction to the category of sequential spaces is full.
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 the double negation topology $\neg\neg$). 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 $\mathcal{E}:=Sh_J(\Sigma)$ allows one to represent the geometric realization functor $sSet \to \mathcal{E}$ as the inverse image of a geometric morphism from $\mathcal{E}$ to the topos of simplicial sets. As Johnstone points out, this approach fails for the big topos on $Top$ and also for Lawvere’s topos for continuum mechanics.
In the internal logic of the topological topos, the limited principle of omniscience (LPO) for the natural numbers is false (and thus excluded middle also fails). Specifically, the space $\mathbb{N}^+$ can be constructed internally as the subset of $2^{\mathbb{N}}$ consisting of non-decreasing sequences, and the discrete space $\mathbb{N}+1$ includes into it as the set of sequences that are 1 at exactly one place or 0 everywhere. Thus, the non-isomorphy of this map exhibits the failure of LPO.
Since the topological topos is generated by $\mathbb{N}^+$, it is in some sense a “canonical” topos where LPO fails. Moreover, if we localize at the inclusion $\mathbb{N}+1 \to \mathbb{N}^+$, we get the subtopos of codiscrete objects, which is equivalent to $Set$; so “forcing LPO to hold gives classical logic.
On the other hand, the lesser limited principle of omniscience (LLPO) does hold in the topological topos. This is easiest to see from its “analytic” version, which is equivalent to saying that every real number $x$ is either $\ge 0$ or $\le 0$. Equivalently, this means that $(-\infty,0] + [0,\infty) \to \mathbb{R}$ is surjective. This follows from Johnstone’s Proposition 6.2 on the preservation of closed unions, which implies that $\mathbb{R}$ is the pushout of $(-\infty,0]$ and $[0,\infty)$ over $\{0\}$.
In particular, as Johnstone remarks, this implies that the quotient $[0,1]/(0\sim 1)$ of the unit interval identifying its endpoints coincides with a “correct” constructive definition of the circle $S^1 = \mathbb{R}/\mathbb{Z}$. It also implies that “every real number has a decimal expansion” (though there is no function assigning to every real number a decimal expansion, since no such function can be continuous).
One of the important facts about the topological topos is that its real numbers object is the set of classical real numbers equipped with its usual topology — or more precisely, with the structure of subsequential space given by the usual notion of convergence for sequences of real numbers (arising from the usual Euclidean topology).
In fact, there are two commonly used definitions of “real number” in a topos: the Dedekind real numbers and the Cauchy real numbers. In a general topos the two may not coincide, although they do coincide if the topos is Boolean or satisfies the axiom of countable choice. The topological topos is not Boolean and might not satisfy countable choice (this is unclear at the moment); but in any case the two real numbers objects nevertheless do coincide therein, and both are the set of classical real numbers with its usual topology.
For the Dedekind real numbers, a proof of this can be found in Johnstone’s paper. Here we sketch a proof for the Cauchy reals.
The Cauchy real numbers object in the topological topos $\mathcal{E}$ is the classical set of real numbers with its usual notion of sequential convergence.
For simplicity, we use Cauchy sequences with a fixed modulus: $x:\mathbb{N} \to \mathbb{Q}$ is Cauchy if ${|x_m - x_n|} \lt \frac{1}{m+1} + \frac{1}{n+1}$ for all $m,n$. Note that if $y$ is the limit of such a Cauchy sequence, then ${|y - x_n|} \le \frac{1}{n+1}$ for all $n$, so convergence also has a fixed modulus.
Since the inverse image functor $\Delta : Set \to \mathcal{E}$ preserves natural numbers objects, the NNO $\mathbb{N}$ of $\mathcal{E}$ has the discrete structure (only eventually-constant sequences converge). And since $\mathbb{Q} \cong \mathbb{N}$ constructively, the “rational numbers object” $\mathbb{Q}$ of $\mathcal{E}$ is also discrete. It follows, by definition of exponentials in $\mathcal{E}$, that the object $\mathbb{Q}^{\mathbb{N}}$ of sequences of rational numbers has the topology of “pointwise-eventually-constant convergence”: a sequence of sequences $((x_{n,k})_k)_n$ converges to a sequence $(y_k)_k$ if for each $k$ the sequence $(x_{n,k})_n$ is eventually constant at $y_k$.
Now the object of Cauchy sequences is a subobject of $\mathbb{Q}^{\mathbb{N}}$ defined by
The predicate ${|x_m - x_n|} \lt \frac{1}{m+1} + \frac{1}{n+1}$ defines a subobject of $\mathbb{Q}^{\mathbb{N}} \times \mathbb{N}\times \mathbb{N}$, which is the pullback of the predicate $\lt$ on $\mathbb{Q}\times\mathbb{Q}$ along the map $\mathbb{Q}^{\mathbb{N}} \times \mathbb{N}\times \mathbb{N} \to \mathbb{Q}\times\mathbb{Q}$ defined by $(x,m,n) \mapsto ({|x_m-x_n|},\frac{1}{m+1}+\frac{1}{n+1})$. Now $\mathbb{Q}\times \mathbb{Q}$ is discrete, and every subobject of a discrete object in $\mathcal{E}$ is (discrete and) relatively codiscrete, i.e. it has the induced topology. Thus, the predicate ${|x_m - x_n|} \lt \frac{1}{m+1} + \frac{1}{n+1}$ also has the induced topology. And since relatively codiscrete maps are the modal maps for a modality, they are closed under arbitrary universal quantification. So the object of Cauchy sequences has the topology induced from $\mathbb{Q}^{\mathbb{N}}$ of pointwise eventually constant convergence.
In any topos, there is a monomorphism from the Cauchy real numbers to the Dedekind real numbers, and as remarked above, Johnstone proved that the latter have the usual topology. Moreover, it is easy to see that the points of the Cauchy real numbers object are precisely the classical real numbers: any classical Cauchy sequence certainly induces a Cauchy sequence internal to $\mathcal{E}$. Thus, it will suffice to show that the Cauchy subobject of the Dedekind reals also contains all convergent sequences.
To this end, suppose we have a sequence of Cauchy sequences $((x_{n,k})_k)_n$ and a Cauchy sequence $(y_k)_k$ (all in the above fixed-modulus sense) such that the sequence of real numbers $([x_n])_n$ converges to the real number $[y]$ in the usual sense. We want to show that this convergence also happens in the Cauchy real numbers object. To this end, define a new sequence of Cauchy sequences $z_{n,k}$ by setting $z_{n,k} = y_{2k+1}$ if ${|[x_n] - y_{2k+1}|} \lt \frac{1}{k+1}$ and $z_{n,k} = x_{n,k}$ otherwise. To show that $z_n$ is Cauchy, the only nontrivial case is to show that ${|y_{2k+1} - x_{n,\ell}|} \lt \frac{1}{k+1} + \frac{1}{\ell+1}$ if ${|[x_n] - y_{2k+1}|} \lt \frac{1}{k+1}$; but since $x_{n,\ell}$ converges to $[x_n]$ with fixed modulus, we have ${|[x_n] - x_{n,\ell}|} \le \frac{1}{\ell+1}$ and the triangle inequality is our friend.
It is also evident that $z_n$ converges to $[x_n]$, i.e. $[z_n] = [x_n]$. Thus it will suffice to show that $([z_n])_n$ converges to $[y]$ in the Cauchy real numbers object. Let $w_k = y_{2k+1}$; then $[w]=[y]$ and $w$ converges twice as fast, i.e. ${|[w] - w_k|} \le \frac{1}{2(k+1)}$. We claim that $((z_{n,k})_k)_n$ is pointwise-eventually-constant convergent to $w_k$. To see this, by the ordinary convergence of $[x_n]$ to $[y]$, for each $k$ there exists an $N$ such that $n\gt N$ implies ${|[x_n] - [w]|}\lt \frac{1}{2(k+1)}$, and hence by the triangle inequality ${|[x_n] - y_{2k+1}|} = {|[x_n] - w_{k}|} \lt \frac{1}{k+1}$. Thus, by definition of $z_n$, we have $z_{n,k} = w_k$ for all $n\gt N$, which is to say that $(z_{n,k})_n$ is eventually constant at $w_k$.
Finally, since $((z_{n,k})_k)_n$ converges to $w_k$ in the object of Cauchy sequences, the image sequence $([z_n])_n$ in the object of Cauchy real numbers (the quotient by equivalence of Cauchy sequences) must also converge to $[w]$ there. Since $[z_n]=[x_n]$ and $[w]=[y]$, this is what we wanted.
The topological topos was introduced in
Peter Johnstone, Topos Theory , Academic Press New York 1977. (Dover reprint 2014; exercise 0.10, p.21)
Peter Johnstone, On a topological topos , Proc. London Math. Soc. (3) 38 (1979) pp.237–271. (pdf)
Some information with a somewhat changed terminology can be found in
The topological topos is discussed in the context of convenient categories of spaces in
Recently, the topos has received attention in the context of Homotopy type theory:
Martín Escardó, Thomas Streicher, The intrinsic topology of Martin-Lof universes, APAL (2016). (pdf)
Bas Spitters, Cubical sets and the topological topos , arXiv:1610.05270 (2016). (abstract)
Generalizations of its construction 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)