\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{Johnstone&#39;s topological topos}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{internal_logic}{Internal logic}\dotfill \pageref*{internal_logic} \linebreak
\noindent\hyperlink{the_real_numbers}{The real numbers}\dotfill \pageref*{the_real_numbers} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak
\noindent\hyperlink{links}{Links}\dotfill \pageref*{links} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

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 \textbf{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.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

Let [[Top]] be the [[category]] of [[topological space]]s, and let $\Sigma$ be the [[full subcategory]] whose only two [[object]]s are a one-point space and $\mathbb{N}^+$, the [[one-point compactification]] of the [[discrete space]] of [[natural number]]s. Let $J$ be the [[canonical Grothendieck topology]] on $\Sigma$.

Johnstone's \textbf{topological topos} (specifically, the one described in the \hyperlink{Johnstone79}{eponymous paper}) is the [[topos]] of canonical [[sheaves]] $Sh_J(\Sigma)$ on $\Sigma$. The functor

\begin{displaymath}
Top \to Set^{\Sigma^{op}}: X \mapsto Top(-, X)
\end{displaymath}
is [[faithful functor|faithful]] and factors through $Sh_J(\Sigma)$, and its restriction to the category of [[sequential space|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|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} \coloneqq 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 set|simplicial sets]]. As Johnstone points out, this approach fails for the [[big topos]] on $Top$ and also for Lawvere's topos for [[continuum mechanics]].

\hypertarget{internal_logic}{}\subsection*{{Internal logic}}\label{internal_logic}

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 [[localization|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 \emph{lesser} limited principle of omniscience (LLPO) \emph{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 \emph{function} assigning to every real number a decimal expansion, since no such function can be continuous).

\hypertarget{the_real_numbers}{}\subsection*{{The real numbers}}\label{the_real_numbers}

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 topos|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.

\begin{utheorem}
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.

\end{utheorem}
\begin{proof}
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

\begin{displaymath}
\left\{ (x_n) \mid \forall n,m, {|x_m - x_n|} \lt \frac{1}{m+1} + \frac{1}{n+1} \right\}.
\end{displaymath}
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 \emph{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 \emph{sequences}, the image sequence $([z_n])_n$ in the object of Cauchy \emph{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.

\end{proof}
\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

\begin{itemize}%
\item [[gros topos]]


\item [[convenient category of topological spaces]]


\item [[bornological topos]]


\item [[topos of recursive sets|recursive topos]]


\item [[effective topos]]


\item [[generic interval]]


\item [[topological site]]



\end{itemize}
\hypertarget{links}{}\subsection*{{Links}}\label{links}

\begin{itemize}%
\item n-cafe \href{https://golem.ph.utexas.edu/category/2014/04/on_a_topological_topos.html}{blog on Johnstone's paper}

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

The topological topos was introduced in

\begin{itemize}%
\item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press New York 1977. (Dover reprint 2014; exercise 0.10, p.21)


\item [[Peter Johnstone]], \emph{On a topological topos} , Proc. London Math. Soc. (3) \textbf{38} (1979) pp.237--271. (\href{http://plms.oxfordjournals.org/content/s3-38/2/237.full.pdf}{pdf})



\end{itemize}
Some information with a somewhat changed terminology can be found in

\begin{itemize}%
\item [[Peter Johnstone]], \emph{Sketches of an [[Elephant]] vols.I\&II}, Oxford UP 2002. (A2.1.11(j), A2.6.4(c), C2.2.14(b); pp.81,123,537f)

\end{itemize}
The topological topos is discussed in the context of [[convenient category of topological spaces|convenient categories of spaces]] in

\begin{itemize}%
\item H. A. Harasani, \emph{Topos theoretic methods in general topology} , PhD Thesis University of Wales Bangor 1988.

\end{itemize}
Recently, the topos has received attention in the context of [[Homotopy type theory]]. Shulman has shown that there is a [[higher topos]] analogue which models [[homotopy type theory]].

\begin{itemize}%
\item [[Michael Shulman]], \emph{Brouwer's fixed-point theorem in real-cohesive homotopy type theory}, 2015 \href{https://arxiv.org/abs/1509.07584}{arXiv}


\item [[Martín Escardó]], [[Thomas Streicher]], \emph{The intrinsic topology of Martin-Lof universes}, APAL (2016). (\href{http://www.cs.bham.ac.uk/~mhe/papers/universe-indiscrete.pdf}{pdf})


\item [[Bas Spitters]], \emph{Cubical sets and the topological topos} , arXiv:1610.05270 (2016). (\href{https://arxiv.org/abs/1610.05270}{abstract})



\end{itemize}
Generalizations of its construction occur in the following two papers:

\begin{itemize}%
\item R. Monta\~n{}ez, \emph{Topoi generated by topological spaces} , Talk CT15 Aveiro 2015. (\href{http://sweet.ua.pt/dirk/ct2015/slides/Montanez.pdf}{pdf-slides})


\item C. Ruiz, R. Monta\~n{}ez, \emph{Elevadores de Estructura} , Bolet\'i{}n de Matem\'a{}ticas \textbf{XIII} no.2 (2006) pp.111--135. (\href{http://www.revistas.unal.edu.co/index.php/bolma/article/view/40451}{link})



\end{itemize}
[[!redirects topological topos]]



\end{document}