\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*{real numbers object}

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

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

[[!include topos theory - contents]]

\hypertarget{real_numbers_object}{}\section*{{Real numbers object}}\label{real_numbers_object}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{constructions}{Constructions}\dotfill \pageref*{constructions} \linebreak
\noindent\hyperlink{in_a_topos_with_an_nno}{In a topos with an NNO}\dotfill \pageref*{in_a_topos_with_an_nno} \linebreak
\noindent\hyperlink{in_a_pretopos_with_}{In a $\Pi$-pretopos with $WCC$}\dotfill \pageref*{in_a_pretopos_with_} \linebreak
\noindent\hyperlink{in_a_pretopos_with_an_nno_and_subset_collection}{In a $\Pi$-pretopos with an NNO and subset collection}\dotfill \pageref*{in_a_pretopos_with_an_nno_and_subset_collection} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{in_}{In $Set$}\dotfill \pageref*{in_} \linebreak
\noindent\hyperlink{in_sheaves_on_a_topological_space}{In sheaves on a topological space}\dotfill \pageref*{in_sheaves_on_a_topological_space} \linebreak
\noindent\hyperlink{InGrosToposOnTopologicalSpaces}{In sheaves on a gros site of topological spaces}\dotfill \pageref*{InGrosToposOnTopologicalSpaces} \linebreak
\noindent\hyperlink{InASheafTopos}{In a general sheaf topos}\dotfill \pageref*{InASheafTopos} \linebreak
\noindent\hyperlink{generalizations}{Generalizations}\dotfill \pageref*{generalizations} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

Recall that it is possible to define an [[internalization]] of the set of [[natural numbers]], called a [[natural numbers object]] (NNO), in any [[cartesian monoidal category]] (a category with finite [[product|products]]). In particular, the notion makes sense in a [[topos]]. But a topos supports [[intuitionistic logic|intuitionistic]] [[higher-order logic]], so once we have an NNO, it is also possible to repeat the usual construction of the [[integer|integers]], the [[rational number|rationals]], and then finally the [[real number|real numbers]]; we thus obtain an internalization of $\mathbb{R}$ in any topos with an NNO.

More generally, we can define a real numbers object (RNO) in any category with sufficient structure (somewhere between a cartesian monoidal category and a topos). Then we can prove that an RNO exists in any topos with an NNO (and in some other situations).

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

Let $\mathcal{E}$ be a [[Heyting category]]. (This means, in particular, that we can interpret full [[first-order logic|first-order]] [[intuitionistic logic]] using the [[stack semantics]].)

\begin{defn}
\label{}\hypertarget{}{}
A (located Dedekind) \textbf{real numbers object} in $\mathcal{E}$ is a [[ring object]] in $\mathcal{E}$ that satisfies (in the [[internal logic]]) the axioms of a [[Dedekind-complete]] [[linearly ordered]] [[Heyting field]].

\end{defn}
In detail:

A \emph{commutative ring object} in $\mathcal{E}$ is an object $R$ equipped with morphisms $0\colon \mathbf{1} \to R$, ${-}\colon R \to R$, ${+}\colon R \times R \to R$, $1\colon \mathbf{1} \to R$, and ${\cdot}\colon R \times R \to R$ (where $\mathbf{1}$ is the [[terminal object]] of $\mathcal{E}$ and $\times$ is the [[product]] operation in $\mathcal{E}$) that make certain diagrams commute. (These diagrams may be found at [[ring object]], in principle, although right now they're not there.)

Given a commutative ring object $R$ in $\mathcal{E}$, we define a [[binary relation]] $\#$ on $R$ (that is a [[subobject]] of $R \times R$) as

\begin{displaymath}
\{ (x,y)\colon R \times R \;|\; \exists z\colon R.\, x \cdot z = y \cdot z + 1 \} ,
\end{displaymath}
written in the [[internal language]] of $\mathcal{E}$. Then $R$ is a (Heyting) \emph{field object} if $\#$ is a tight [[apartness relation]]; that is if the following axioms (in the internal language) hold:

\begin{itemize}%
\item [[irreflexive relation|irreflexivity]]: $\forall x\colon R.\, \neg(x \# x)$,
\item [[symmetric relation|symmetry]]: $\forall x\colon R.\, \forall y\colon R.\, (x \# y \implies y \# x)$ (which can actually be proved using $-$),
\item [[comparison relation|comparison]]: $\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, (x \# z \implies (x \# y \vee y \# z))$,
\item [[tight relation|tightness]]: $\forall x\colon R.\, \forall y\colon R.\, (\neg(x \# y) \implies x = y)$.

\end{itemize}
A (linearly) \emph{ordered field object} in $\mathcal{E}$ is a field object $R$ equipped with a binary relation $\lt$ such that the following axioms hold:

\begin{itemize}%
\item strong [[irreflexive relation|irreflexivity]]: $\forall x\colon R.\, \forall y\colon R.\, (x \lt y \implies x \# y)$,
\item strong [[connected relation|connectedness]]: $\forall x\colon R.\, \forall y\colon R.\, (x \# y \implies (x \lt y \vee y \lt x))$,
\item [[transitive relation|transitivity]]: $\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, ((x \lt y \wedge y \lt z) \implies x \lt z)$,
\item respecting addition: $\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, (x \lt y \implies x + z \lt y + z)$,
\item respecting multiplication: $\forall x\colon R.\, \forall y\colon R.\, \forall z\colon R.\, ((x \lt y \wedge 0 \lt z) \implies x \cdot z \lt y \cdot z)$.

\end{itemize}
Given an ordered field object $R$ in $\mathcal{E}$, any object $\Gamma$ in $\mathcal{E}$, and subobjects $L$ and $U$ of $\Gamma \times R$, we say that $(L,U)$ is a \emph{Dedekind cut} in $R$ (parametrised by $\Gamma$) if the following axioms hold:

\begin{itemize}%
\item lower bound: $\forall a\colon \Gamma.\, \exists x\colon R.\, (a,x) \in L$,
\item upper bound: $\forall a\colon \Gamma.\, \exists x\colon R.\, (a,x) \in U$,
\item downward roundedness: $\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, ((x \lt y \wedge (a,y) \in L) \implies (a,x) \in L)$,
\item upward roundedness: $\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, (((a,x) \in U \wedge x \lt y) \implies (a,y) \in U)$,
\item upward openness: $\forall a\colon \Gamma.\, \forall x\colon R.\, ((a,x) \in L \implies \exists b\colon \Gamma.\, \exists y\colon R.\, ((b,y) \in L \wedge x \lt y))$,
\item downward openness: $\forall a\colon \Gamma.\, \forall x\colon R.\, ((a,x) \in U \implies \exists b\colon \Gamma.\, \exists y\colon R.\, ((b,y) \in U \wedge y \lt x))$,
\item locatedness: $\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, (x \lt y \implies ((a,x) \in L \vee (a,y) \in U))$,
\item separation: $\forall a\colon \Gamma.\, \forall x\colon R.\, \forall y\colon R.\, (((a,x) \in L \wedge (a,y) \in U) \implies x \lt y)$.

\end{itemize}
An ordered field object $R$ in $\mathcal{E}$ is \emph{Dedekind complete} if, given any object $\Gamma$ of $\mathcal{E}$ and any Dedekind cut $(L,U)$ in $R$ parametrised by $\Gamma$, there exists a morphism $x\colon \Gamma \to R$ such that

\begin{displaymath}
L = \{ (a,b)\colon \Gamma \times R \;|\; b \lt x(a) \} ,
\end{displaymath}
\begin{displaymath}
U = \{ (a,b)\colon \Gamma \times R \;|\; x(a) \lt b \} .
\end{displaymath}
Finally, a \emph{real numbers object} in $\mathcal{E}$ is a Dedekind-complete ordered field object.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

In the last requirement, of Dedekind completeness, we postulate (under certain conditions) the existence of a morphism $x\colon \Gamma \to R$ satisfying certain properties.

\begin{thm}
\label{}\hypertarget{}{}
This morphism is in fact unique.

\end{thm}
Here is an explicit `external' proof:

\begin{proof}
Suppose that $x, x'\colon \Gamma \to R$ both satisfy the required properties, and consider $x \# x'$, which is a subobject of $\Gamma$. By the strong connectedness of $\lt$, $x \# x'$ is contained in (factors through) $x \lt x' \vee x' \lt x$, which is the [[union]] of $x \lt x'$ and $x' \lt x$.

Now consider $x \lt x'$, and let $a$ be a [[generalised element]] of $\Gamma$. If $a$ belongs to (factors through) $x \lt x'$, or equivalently $(x(a), x'(a))$ belongs to $\lt$, it follows that $(a,x(a))$ belongs to $L$. Thus, $(x(a), x(a))$ also belongs to $\lt$, or equivalently $a$ belongs to $x \lt x$. By the strong irreflexivity of $\lt$, this is contained in $x \# x$; by the irreflexivity of $\#$, this is contained in $\bot$ (as a subobject of $\Gamma$). Since every $a$ that belongs to $x \lt x'$ belongs to $\bot$, $x \lt x'$ is contained in (and so equals as a subobject) $\bot$.

Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also $\bot$. Therefore, $x \# x'$ is $\bot$. By the tightness of $\#$, $x = x'$.

\end{proof}
Here is an `internal' proof, to be interpreted in the [[stack semantics]] of $\mathcal{E}$:

\begin{proof}
Suppose that $x, x'\colon R$ both satisfy the required properties, and suppose that $x \# x'$. By the strong connectedness of $\lt$, $x \lt x'$ or $x' \lt x$.

Now suppose that $x \lt x'$. It follows that $x$ belongs to $L$, so $x \lt x$. By the strong irreflexivity of $\lt$, $x \# x$; by the irreflexivity of $\#$, we have a contradiction.

Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also false. Therefore, $x \# x'$ is false. By the tightness of $\#$, $x = x'$.

\end{proof}
In the definition of a Heyting field object, all of the axioms except the last are [[coherent logic|coherent]] and therefore make sense in any [[coherent category]].

\begin{thm}
\label{}\hypertarget{}{}
An object satisfying all but the last axiom of a field object is precisely a [[local ring]] object (so in particular an RNO is a local ring object).

\end{thm}
\begin{proof}
\ldots{}

\end{proof}
It would be nice to say that a Heyting category with an RNO must have an NNO; after all, $\mathbb{N}$ is contained in $\mathbb{R}$. However, my only argument is impredicative; although I don't know a specific example, there could be a [[Π-pretopos]] with an RNO but no NNO. However, the argument works for a [[infinitary coherent category|geometric]] Heyting category or a [[topos]]. (In light of the constructions below, the existence of an RNO is therefore equivalent to the existence of an NNO in a topos.)

\begin{thm}
\label{}\hypertarget{}{}
If $R$ is an RNO in an infinitary Heyting category or topos, then there is unique subobject $N$ of $R$ that is both a sub-[[rig]] object of $R$ and an NNO under the operations $0\colon \mathbf{1} \to N$ and $({-}) + 1\colon N \to N$.

\end{thm}
\begin{proof}
\ldots{}

\end{proof}
We usually speak of \emph{[[the]]} RNO, if one exists. This is because any two RNOs in a Heyting category with an NNO are [[isomorphic]], in an essentially unique way. (I can't prove this without an NNO, although the previous theorem shows that we often have one.)

\begin{thm}
\label{}\hypertarget{}{}
If $R$ and $R'$ are both RNOs in a Heyting category $\mathcal{E}$ with an NNO, then there is a unique isomorphism from $R$ to $R'$ that preserves the structures on them ($0$, $-$, $+$, $1$, $\cdot$, $\lt$).

\end{thm}
\begin{proof}
\ldots{}

\end{proof}
\hypertarget{constructions}{}\subsection*{{Constructions}}\label{constructions}

We can construct a real numbers object in the following cases (presumably among others):

\begin{enumerate}%
\item in a topos with an NNO;
\item in a $\Pi$-[[Pi-pretopos|pretopos]] with an NNO and [[weak countable choice]];
\item in a $\Pi$-pretopos with an NNO and [[subset collection]].

\end{enumerate}
(Actually, (1) is a special case of (3), but the usual construction in (1) is not available in (3). Thus, we still have three different constructions to consider.)

\hypertarget{in_a_topos_with_an_nno}{}\subsubsection*{{In a topos with an NNO}}\label{in_a_topos_with_an_nno}

Let $\mathcal{E}$ be an [[elementary topos]] with a natural numbers object $\mathbb{N}$. The \textbf{Dedekind real numbers object} of $\mathcal{E}$ is the object of all [[Dedekind cut|Dedekind cuts]]. To be more precise, we will need to make some auxiliary definitions.

We first construct an integers object as follows. Let $a, b\colon E \to \mathbb{N} \times \mathbb{N}$ be the [[kernel pair]] of the addition map ${+}\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}$, and let $\pi_1, \pi_2\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be the [[product]] projections. We define $\mathbb{Z}$ to be the [[coequalizer]] of $(\pi_1 \circ a, \pi_2 \circ b), (\pi_2 \circ a, \pi_1 \circ b)\colon E \to \mathbb{N}$. A similar construction yields a rational numbers object $\mathbb{Q}$.

We denote by $\mathcal{P}(A)$ the [[power object]] of $A$ in $\mathcal{E}$. A \textbf{Dedekind cut} is a [[generalized element]] $(L, U)$ of $\mathcal{P}(\mathbb{Q}) \times \mathcal{P}(\mathbb{Q})$, satisfying the following conditions, expressed in the [[Mitchell?Bénabou language]] of $\mathcal{E}$ and interpreted under [[Kripke-Joyal semantics|Kripke?Joyal semantics]]:

\begin{enumerate}%
\item Non-degenerate:

\begin{displaymath}
\exists q\colon \mathbb{Q}.\, q \in L ;
\end{displaymath}
\begin{displaymath}
\exists r\colon \mathbb{Q}.\, r \in U .
\end{displaymath}

\item Inward-closed:

\begin{displaymath}
\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((q \lt r \wedge r \in L) \implies q \in L) ;
\end{displaymath}
\begin{displaymath}
\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, ((r \lt q \wedge r \in U) \implies q \in U) .
\end{displaymath}

\item Outward-open:

\begin{displaymath}
\forall q\colon \mathbb{Q}.\, (q \in L \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge q \lt r))
\end{displaymath}
\begin{displaymath}
\forall q\colon \mathbb{Q}.\, (q \in U \implies \exists r\colon \mathbb{Q}.\, (r \in L \wedge r \lt q)) .
\end{displaymath}

\item Located:

\begin{displaymath}
\forall q\colon \mathbb{Q}.\, \forall r\colon \mathbb{Q}.\, (q \lt r \implies (q \in L \vee r \in U)) .
\end{displaymath}

\item Mutually exclusive:

\begin{displaymath}
\forall q\colon \mathbb{Q}.\, \neg(q \in L \wedge q \in U) .
\end{displaymath}


\end{enumerate}
The relation $\lt$ on $\mathbb{Q}$ is the order relation constructed in the usual way. We define $\mathbb{R}$ to be the subobject of $\mathcal{P}(\mathbb{Q}) \times \mathcal{P}(\mathbb{Q})$ consisting of all Dedekind cuts as defined above.

\hypertarget{in_a_pretopos_with_}{}\subsubsection*{{In a $\Pi$-pretopos with $WCC$}}\label{in_a_pretopos_with_}

Summary: construct a [[Cauchy real numbers]] object and use $WCC$ ([[weak countable choice]]) to prove that it is an RNO.

Note that any [[Boolean topos]] with an NNO satisfies $WCC$, so in all we have three different constructions available in that case.

\hypertarget{in_a_pretopos_with_an_nno_and_subset_collection}{}\subsubsection*{{In a $\Pi$-pretopos with an NNO and subset collection}}\label{in_a_pretopos_with_an_nno_and_subset_collection}

Summary: modify the construction of a [[Cauchy real numbers]] object to use [[multi-valued function|multi-valued]] [[Cauchy sequences]].

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{in_}{}\subsubsection*{{In $Set$}}\label{in_}

The real numbers object in [[Set]] is the [[real line]], the usual set of (located Dedekind) [[real numbers]]. Note that this is a theorem of [[constructive mathematics]], as long as we assume that $Set$ is an elementary topos with an NNO (or more generally a [[Π-pretopos]] with [[natural numbers object|NNO]] and either WCC or subset collection).

\hypertarget{in_sheaves_on_a_topological_space}{}\subsubsection*{{In sheaves on a topological space}}\label{in_sheaves_on_a_topological_space}

Let $X$ be a [[topological space]], and $\mathrm{Sh}(X)$ its [[category of sheaves]]. It is well-known that $\mathrm{Sh}(X)$ is a [[Grothendieck topos]] (and so, \emph{a fortiori}, an elementary topos), and the [[constant sheaf]] [[functor]] $\Delta\colon \mathbf{Set} \to \mathrm{Sh}(X)$ preserves [[finite limits]] and has the [[global section]] functor $\Gamma\colon \mathrm{Sh}(X) \to \mathbf{Set}$ as a [[right adjoint]]. (Hence, $\Delta$ and $\Gamma$ are the components of a [[geometric morphism]] $\mathrm{Sh}(X) \to \mathbf{Set}$.) The following claims are essentially immediate:

\begin{enumerate}%
\item If $\mathbf{N}$ is the set of natural numbers, then $\Delta (\mathbf{N})$ must be an NNO in $\mathrm{Sh}(X)$, since $\Delta$ has a right adjoint.


\item If $\mathbf{Z}$ is the set of integers, then $\Delta (\mathbf{Z})$ is an integers object in $\mathrm{Sh}(X)$ (as defined above), since $\Delta$ preserves finite limits and colimits.


\item Similarly, if $\mathbf{Q}$ is the set of rational numbers, then $\Delta (\mathbf{Q})$ is a rational numbers object in $\mathrm{Sh}(X)$.



\end{enumerate}
Thus, for every topological space $X$, the topos $\mathrm{Sh}(X)$ has a Dedekind real numbers object $\mathbb{R}$. Na\"i{}vely one might expect $\mathbb{R}$ to be isomorphic to the constant sheaf $\Delta(\mathbf{R})$, where $\mathbf{R}$ is the classical set of real numbers, but this turns out not to be the case. Instead, we have a rather more remarkable result:

\begin{theorem}
\label{DedekindRealsInToposOverTopologicalSpace}\hypertarget{DedekindRealsInToposOverTopologicalSpace}{}
A Dedekind real numbers object $\mathbb{R}$ in the topos $\mathrm{Sh}(X)$ is isomorphic to the sheaf of real-valued [[continuous functions]] on $X$.

\end{theorem}
This is shown in (\hyperlink{MM94}{MacLane-Moerdijk, Chapter VI, \S{}8, theorem 2}); see also below.

\begin{remark}
\label{}\hypertarget{}{}
Theorem \ref{DedekindRealsInToposOverTopologicalSpace} allows us to define various further constructions on $X$ in internal terms in $\mathrm{Sh}(X)$; for example, a [[vector bundle]] over $X$ is an internal [[projective object|projective]] $\mathbb{R}$-[[module]].

\end{remark}
\hypertarget{InGrosToposOnTopologicalSpaces}{}\subsubsection*{{In sheaves on a gros site of topological spaces}}\label{InGrosToposOnTopologicalSpaces}

\begin{theorem}
\label{}\hypertarget{}{}
Let $\{\mathbb{R}\} \hookrightarrow S \hookrightarrow Top$ be a [[small category|small]] [[full subcategory]] of [[Top]] including the [[real line]]. If $S$ is closed under forming [[open subspaces]] and pullbacks of open subspaces and we equip it with the open-cover [[coverage]], then the Dedekind real number object internal to $Sh(S)$ is [[representable functor|represented]] by $\mathbb{R}^1$.

\end{theorem}
This is proven as (\hyperlink{MM94}{MacLane-Moerdijk, chapter VI \S{}9, theorem 2}) under the stronger assumption that $S$ is closed under open subspaces and finite limits, by showing that over each object in the site the argument reduces essentially to that of theorem \ref{DedekindRealsInToposOverTopologicalSpace} for that object. However, the finite limits are not necessary; see also below. The more general version includes the cases

\begin{itemize}%
\item $S =$ $\{$ [[locally contractible topological spaces]] $\}$


\item $S =$ $\{$ [[topological manifolds]] $\}$



\end{itemize}
(for which $Sh(S)$ is [[cohesive topos]] and $Sh_\infty(S)$ is an [[cohesive (∞,1)-topos]]).

\hypertarget{InASheafTopos}{}\subsubsection*{{In a general sheaf topos}}\label{InASheafTopos}

We can generalize the above theorem as follows. Let $S$ be any [[site]], and for any object $X\in S$ let $L(X)$ denote the [[locale]] whose [[frame]] of opens is the frame of [[subobjects]] of the sheafified representable $y X \in Sh(S)$. We have an induced functor $L:S\to Loc$. We can also regard the ordinary real numbers $\mathbb{R}$ as a locale.

\begin{theorem}
\label{}\hypertarget{}{}
The Dedekind real number object in $Sh(S)$ is the functor $Loc(L-,\mathbb{R})$.

\end{theorem}
\begin{proof}
The sheaf topos $Sh(\mathbb{R})$ is the classifying topos of the geometric theory of a real number, in the sense that for any Grothendieck topos $E$, geometric morphisms $E \to Sh(\mathbb{R})$ are equivalent to global points of the real numbers object $\mathbb{R}_E$ in $E$. Since pullback functors are logical, they preserve the real numbers object; thus for any $X\in E$, maps $X\to \mathbb{R}_E$ are equivalent to geometric morphisms $E/X \to Sh(\mathbb{R})$. But $Sh(\mathbb{R})$ is localic, so such geometric morphisms factor through the localic reflection of $E/X$, and therefore are equivalent to continuous $\mathbb{R}$-valued functions defined on the ``little locale of $X$'', i.e. the locale associated to the frame of subobjects of $X$ in $E$.

Therefore, if $E = Sh(S)$ for some site $S$, then $\mathbb{R}_E$ is the sheaf on $S$ where $\mathbb{R}_E(X)=$ the set of continuous $\mathbb{R}$-valued functions on the little locale of $y X \in E$, which is what we have called $L X$.

\end{proof}
To deduce the previous theorem from this one, it suffices to observe that if $S\subset Top$ is closed under open subspaces and their pullbacks and equipped with the open-cover coverage, then every subobject of $y X\in Sh(S)$, for any $X\in S$, is uniquely representable by an open subset of $X$.

There is some dispute about this, see \href{http://nforum.mathforge.org/discussion/6289/when-is-the-internal-real-line-the-external-real-line/?Focus=50275#Comment_50275}{here}.

Resolution seems to be \href{http://mathoverflow.net/a/186165/381}{here}

\hypertarget{generalizations}{}\subsection*{{Generalizations}}\label{generalizations}

It is also possible to define the notion of a [[Cauchy real number]] object and construct one in any $\Pi$-pretopos with an NNO, but as the internal logic in general lacks [[weak countable choice]], these are usually inequivalent. (There is also potentially a difference between the \emph{classical} Cauchy RNO and the \emph{modulated} Cauchy RNO; see definitions at [[Cauchy real number]], to be interpreted in the [[stack semantics]].)

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[real number]]


\item [[Cauchy real number]]


\item [[one-sided real numbers]]


\item [[natural number]]


\item [[natural numbers object]]


\item [[smooth structure on a topos]]



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

Discussion in [[topos theory]] is in

\begin{itemize}%
\item [[Peter Johnstone]], section D4.7 of \emph{[[Sketches of an Elephant]]}


\item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press New York 1977 (Dover reprint New York 2014). (section 6.6. pp.210-23)


\item [[Saunders Mac Lane]], [[Ieke Moerdijk]], section VI.8 of \emph{[[Sheaves in Geometry and Logic]]} .


\item [[Eduardo Dubuc]], \emph{Logical Opens and Real Numbers in Topoi} , JPAA \textbf{43} (1986) pp.129-143.


\item [[Michael Fourman]], \emph{Comparaison des R\'e{}els d'un Topos - Structures Lisses sur un Topos El\'e{}mentaire} , Cah. Top. G\'e{}om. Diff. Cat. \textbf{16} (1975) pp.233-239. ( \emph{Colloque Amiens 1975 proceedings} ) (p. 18-24 in \href{http://www.numdam.org/item?id=CTGDC_1975__16_3_217_0}{NUMDAM}))


\item [[Michael Fourman]], \emph{T$_1$ Spaces over Topological Sites} , JPAA \textbf{27} (1983) pp.223-224.


\item [[Michael Fourman]], [[Martin Hyland]], \emph{Sheaf Models for Analysis} , pp.280-301 in Fourman, Mulvey, Scott (eds.), \emph{Applications of Sheaves} , LNM \textbf{753} Springer Heidelberg 1979. (\href{https://www.dpmms.cam.ac.uk/~martin/Research/Oldpapers/analysis79.pdf}{draft}, 6.64 MB)


\item [[André Joyal]], [[Gonzalo E. Reyes]], \emph{Separably Real Closed Local Rings} , JPAA \textbf{43} (1986) pp.271--279.


\item [[Ieke Moerdijk]], [[Gonzalo E. Reyes]], \emph{Smooth Spaces versus Continuous Spaces in Models of Synthetic Differential Geometry} , JPAA \textbf{32} (1984) pp.143-176.


\item J. Z. Reichman, \emph{Semicontinuous Real Numbers in a Topos} , JPAA \textbf{28} (1983) pp.81-91.


\item L. Stout, \emph{Unpleasant Properties of the Reals in a Topos} , Cah. Top. G\'e{}om. Diff. Cat. \textbf{16} (1975) pp.320-322. (\href{http://archive.numdam.org/ARCHIVE/CTGDC/CTGDC_1975__16_3/CTGDC_1975__16_3_217_0/CTGDC_1975__16_3_217_0.pdf}{Colloque Amiens 1975 proceedings},6.81 MB)


\item L. N. Stout, \emph{Topological Properties of the Real Numbers Object in a Topos} , Cah. Top. G\'e{}om. Diff. Cat. \textbf{17} no.3 (1976) pp.295-326. (\href{http://archive.numdam.org/ARCHIVE/CTGDC/CTGDC_1976__17_3/CTGDC_1976__17_3_295_0/CTGDC_1976__17_3_295_0.pdf}{pdf})



\end{itemize}
Discussion in [[homotopy type theory]] is in

\begin{itemize}%
\item [[Univalent Foundations Project]], section 11 of \emph{[[Homotopy Type Theory -- Univalent Foundations of Mathematics]]}

\end{itemize}
[[!redirects real numbers object]] [[!redirects real numbers objects]] [[!redirects real number object]] [[!redirects real number objects]] [[!redirects real-numbers object]] [[!redirects real-numbers objects]] [[!redirects real-number object]] [[!redirects real-number objects]]

[[!redirects real numbers object in a topos]] [[!redirects real numbers objects in a topos]] [[!redirects real numbers objects in toposes]] [[!redirects real numbers objects in topoi]] [[!redirects real number object in a topos]] [[!redirects real number objects in a topos]] [[!redirects real number objects in toposes]] [[!redirects real number objects in topoi]] [[!redirects real-numbers object in a topos]] [[!redirects real-numbers objects in a topos]] [[!redirects real-numbers objects in toposes]] [[!redirects real-numbers objects in topoi]] [[!redirects real-number object in a topos]] [[!redirects real-number objects in a topos]] [[!redirects real-number objects in toposes]] [[!redirects real-number objects in topoi]]

[[!redirects Dedekind real numbers object]] [[!redirects Dedekind real numbers objects]] [[!redirects Dedekind real number object]] [[!redirects Dedekind real number objects]] [[!redirects Dedekind real-numbers object]] [[!redirects Dedekind real-numbers objects]] [[!redirects Dedekind real-number object]] [[!redirects Dedekind real-number objects]]

[[!redirects Cauchy real numbers object]] [[!redirects Cauchy real numbers objects]] [[!redirects Cauchy real number object]] [[!redirects Cauchy real number objects]] [[!redirects Cauchy real-numbers object]] [[!redirects Cauchy real-numbers objects]] [[!redirects Cauchy real-number object]] [[!redirects Cauchy real-number objects]]



\end{document}