reals.tex

\chapter{Real numbers}
\label{cha:real-numbers}

\index{real numbers|(}%
Any foundation of mathematics worthy of its name must eventually address the construction of real numbers as understood by mathematical analysis, namely as a complete archimedean ordered field.
\index{ordered field}%
There are two notions of completeness. The one by Cauchy requires that the reals be closed under limits of Cauchy sequences\index{Cauchy!sequence}, while the stronger one by Dedekind requires closure under Dedekind cuts.\index{cut!Dedekind}
These lead to two ways of constructing reals, which we study in \cref{sec:dedekind-reals} and \cref{sec:cauchy-reals}, respectively. In \cref{RD-final-field,RC-initial-Cauchy-complete} we characterize the two constructions in terms of universal properties: the Dedekind reals are the final archimedean ordered field, and the Cauchy reals the initial Cauchy complete archimedean ordered field.

In traditional constructive mathematics,
\index{mathematics!constructive}%
real numbers always seem to require certain compromises. For example, the Dedekind reals work better with power sets or some other form of impredicativity, while Cauchy reals work well in the presence of countable choice.
\index{axiom!of choice!countable}%
However, we give a new construction of the Cauchy reals as a higher inductive-inductive type that seems to be a third possibility, which requires neither power sets nor countable choice.

In~\cref{sec:comp-cauchy-dedek} we compare the two constructions of reals. The Cauchy reals are included in the Dedekind reals. They coincide if excluded middle or countable choice holds, but in general the inclusion might be proper.

In~\cref{sec:compactness-interval} we consider three notions of compactness of the closed interval~$[0,1]$. We first show that $[0,1]$ is metrically compact\indexdef{metrically compact}\indexdef{compactness!metric} in the sense that it is complete and totally bounded, and that uniformly continuous maps on metrically compact spaces behave as expected. In contrast, the Bolzano--Weierstra\ss{} property that every sequence has a convergent subsequence implies the limited principle of omniscience, which is an instance of excluded middle. Finally, we discuss Heine--Borel compactness. A naive formulation of the finite subcover property does not work, but a proof relevant notion of inductive covers does.
This section is basically standard constructive analysis.

The development of real numbers and analysis in homotopy type theory can be easily made compatible with classical mathematics. By assuming excluded middle and the axiom of choice we get standard classical analysis:\index{mathematics!classical}\index{classical!analysis} the Dedekind and Cauchy reals coincide, foundational questions about the impredicative nature of the Dedekind reals disappear, and the interval is as compact as it could be.

We close the chapter by constructing Conway's surreals as a higher inductive-inductive type in \cref{sec:surreals};
the construction is more natural in univalent type theory than in  classical set theory.

In addition to the basic theory of \cref{cha:basics,cha:logic}, as noted above we use ``higher inductive-inductive types'' for the Cauchy reals and the surreals: these combine the ideas of \cref{cha:hits} with the notion of inductive-inductive type mentioned in \cref{sec:generalizations}.
We will also frequently use the traditional logical notation described in \cref{subsec:prop-trunc}, and the fact (proven in \cref{sec:piw-pretopos}) that our ``sets'' behave the way we would expect.

Note that the total space of the universal cover of the circle, which
in \cref{subsec:pi1s1-homotopy-theory} played a role similar to ``the real numbers'' in
classical algebraic topology, is \emph{not} the type of reals we are looking for. That
type is contractible, and thus equivalent to the singleton type, so it cannot be equipped
with a non-trivial algebraic structure.



\section{The field of rational numbers}
\label{sec:field-rati-numb}

\indexdef{rational numbers}%
\indexsee{number!rational}{rational numbers}%
We first construct the rational numbers \Q, as the reals can then be seen as a completion
of~\Q. An expert will point out that \Q could be replaced by any approximate field,
\indexdef{field!approximate}%
i.e., a subring of \Q in which arbitrarily precise approximate inverses
\index{inverse!approximate}%
exist. An example is the
ring of dyadic rationals,
\index{rational numbers!dyadic}%
which are those of the form $n/2^k$.
If we were implementing constructive mathematics on a computer,
an approximate field would be more suitable, but we leave such finesse for those
who care about the digits of~$\pi$.

We constructed the integers \Z in \cref{sec:set-quotients} as a quotient of $\N\times
\N$, and observed that this quotient is generated by an idempotent. In
\cref{sec:free-algebras} we saw that \Z is the free group on \unit; we could similarly
show that it is the free commutative ring\index{ring} on \emptyt. The field of rationals \Q is
constructed along the same lines as well, namely as the quotient
%
\[ \Q \defeq (\Z \times \N)/{\approx} \]
%
where
\[ (u,a) \approx (v,b) \defeq (u (b + 1) = v (a + 1)). \]
%
In other words, a pair $(u, a)$ represents the rational number $u / (1 + a)$. There can be
no division by zero because we cunningly added one to the denominator~$a$. Here too we
have a canonical choice of representatives, namely fractions in lowest terms. Thus we may
apply \cref{lem:quotient-when-canonical-representatives} to obtain a set \Q, which
again has a decidable equality.
\index{decidable!equality}%

We do not bother to write down the arithmetical operations on \Q as we trust that our readers
know how to compute with fractions even in the case when one is added to the denominator.
Let us just record the conclusion that there is an entirely unproblematic construction of
the ordered field of rational numbers \Q, with a decidable equality and decidable order.
It can also be characterized as the initial ordered field.
\index{initial!ordered field}%

\symlabel{positive-rationals}
\indexdef{rational numbers!positive}%
\indexdef{positive!rational numbers}%
Let $\Qp = \setof{ q : \Q | q > 0 }$ be the type of positive rational numbers.

\section{Dedekind reals}
\label{sec:dedekind-reals}

\index{real numbers!Dedekind|(}%
Let us first recall the basic idea of Dedekind's construction. We use two-sided Dedekind
cuts, as opposed to an often used one-sided version, because the symmetry makes
constructions more elegant, and it works constructively as well as classically.
\index{mathematics!constructive}%
A \emph{Dedekind cut}\index{cut!Dedekind} consists of a pair $(L, U)$ of subsets $L, U \subseteq \Q$, called the
\emph{lower} and \emph{upper cut} respectively, which are:
%
\begin{enumerate}
\item \emph{inhabited:} there are $q \in L$ and $r \in U$,
\item \emph{rounded:} $q \in L \Leftrightarrow \exis {r \in \Q} q < r \land r \in L$
  and $r \in U \Leftrightarrow \exis {q \in \Q} q \in U \land q < r$,
  \index{rounded!Dedekind cut}
\item \emph{disjoint:} $\lnot (q \in L \land q \in U)$, and
\item \emph{located:} $q < r \Rightarrow q \in L \lor r \in U$.
  \index{locatedness}%
\end{enumerate}
%
Reading the roundedness condition from left to right tells us that cuts are \emph{open},
\index{open!cut}%
and from right to left that they are \emph{lower}, respectively \emph{upper}, sets. The
locatedness condition states that there is no large gap between $L$ and $U$. Because cuts
are always open, they never include the ``point in between'', even when it is rational. A
typical Dedekind cut looks like this:
%
\begin{center}
  \begin{tikzpicture}[x=\textwidth]
    \draw[<-),line width=0.75pt] (0,0) -- (0.297,0) node[anchor=south east]{$L\ $};
    \draw[(->,line width=0.75pt] (0.300, 0) node[anchor=south west]{$\ U$} -- (0.9, 0) ;
  \end{tikzpicture}
\end{center}
%
We might naively translate the informal definition into type theory by saying that a cut
is a pair of maps $L, U : \Q \to \prop$. But we saw in \cref{subsec:prop-subsets} that
$\prop$ is an ambiguous\index{typical ambiguity} notation for $\prop_{\UU_i}$ where~$\UU_i$ is a universe. Once we
use a particular $\UU_i$ to define cuts, the type of reals will reside in the next
universe $\UU_{i+1}$, a property of reals two levels higher in $\UU_{i+2}$, a property of
subsets of reals in $\UU_{i+3}$, etc. In principle we should be able to keep track of the
universe levels\index{universe level}, especially with the help of a proof assistant, but doing so here would
just burden us with bureaucracy that we prefer to avoid. We shall therefore make a
simplifying assumption that a single type of propositions $\Omega$ is sufficient for all
our purposes.

In fact, the construction of the Dedekind reals is quite resilient to logical
manipulations. There are several ways in which we can make sense of using a single type
$\Omega$:
%
\begin{enumerate}

\item We could identify $\Omega$ with the ambiguous $\prop$ and track all the universes
  that appear in definitions and constructions.

\item We could assume the propositional resizing axiom,
  \index{propositional!resizing}%
  as in \cref{subsec:prop-subsets}, which essentially collapses the $\prop_{\UU_i}$'s to the
  lowest level\index{universe level}, which we call $\Omega$.

\item A classical mathematician who is not interested in the intricacies of type-theoretic
  universes or computation may simply assume the law of excluded middle~\eqref{eq:lem} for
  mere propositions so that $\Omega \jdeq \bool$.
  \index{excluded middle}
  This not only eradicates questions about
  levels\index{universe level} of $\prop$, but also turns everything we do into the standard classical\index{mathematics!classical}
  construction of real numbers.

\item On the other end of the spectrum one might ask for a minimal requirement that makes
  the constructions work. The condition that a mere predicate be a Dedekind cut is
  expressible using only conjunctions, disjunctions, and existential quantifiers\index{quantifier!existential} over~\Q, which
  is a countable set. Thus we could take $\Omega$ to be the initial \emph{$\sigma$-frame},
  \index{initial!sigma-frame@$\sigma$-frame}%
  \index{sigma-frame@$\sigma$-frame!initial|defstyle}%
  i.e., a lattice\index{lattice} with countable joins\index{join!in a lattice} in which binary meets distribute over countable
  joins. (The initial $\sigma$-frame cannot be the two-point lattice $\bool$ because
  $\bool$ is not closed under countable joins, unless we assume excluded middle.) This
  would lead to a construction of~$\Omega$ as a higher inductive-inductive type, but one
  experiment of this kind in \cref{sec:cauchy-reals} is enough.
\end{enumerate}

In all of the above cases $\Omega$ is a set.
%
Without further ado, we translate the informal definition into type theory.
Throughout this chapter, we use the
logical notation from \cref{defn:logical-notation}.

\begin{defn} \label{defn:dedekind-reals}
  A \define{Dedekind cut}
  \indexsee{Dedekind!cut}{cut, Dedekind}%
  \indexdef{cut!Dedekind}%
  is a pair $(L, U)$ of mere predicates $L : \Q \to \Omega$ and $U
  : \Q \to \Omega$ which is:
  %
  \begin{enumerate}
  \item \emph{inhabited:} $\exis{q : \Q} L(q)$ and $\exis{r : \Q} U(r)$,
  \item \emph{rounded:} for all $q, r : \Q$,
    \index{rounded!Dedekind cut}
    %
    \begin{align*}
      L(q) &\Leftrightarrow \exis{r : \Q} (q < r) \land L(r)
      \qquad\text{and}\\
      U(r) &\Leftrightarrow \exis{q : \Q} (q < r) \land U(q),
    \end{align*}
  \item \emph{disjoint:} $\lnot (L(q) \land U(q))$ for all $q : \Q$,
  \item \emph{located:} $(q < r) \Rightarrow L(q) \lor U(r)$ for all $q, r : \Q$.
  \index{locatedness}%
  \end{enumerate}
  %
  We let $\dcut(L, U)$ denote the conjunction of these conditions. The type of
  \define{Dedekind reals} is
  \indexsee{Dedekind!real numbers}{real numbers, De\-de\-kind}%
  \indexdef{real numbers!Dedekind}%
  %
  \begin{equation*}
    \RD \defeq \setof{ (L, U) : (\Q \to \Omega) \times (\Q \to \Omega) | \dcut(L,U)}.
  \end{equation*}
\end{defn}

It is apparent that $\dcut(L, U)$ is a mere proposition, and since $\Q \to \Omega$ is a
set the Dedekind reals form a set too. See
\cref{ex:RD-extended-reals,ex:RD-lower-cuts,ex:RD-interval-arithmetic} for variants of
Dedekind cuts which lead to extended reals, lower and upper reals, and the interval
domain.

There is an embedding $\Q \to \RD$ which associates with each rational $q : \Q$ the cut
$(L_q, U_q)$ where
%
\begin{equation*}
  L_q(r) \defeq (r < q)
  \qquad\text{and}\qquad
  U_q(r) \defeq (q < r).
\end{equation*}
%
We shall simply write $q$ for the cut $(L_q, U_q)$ associated with a rational number.

\subsection{The algebraic structure of Dedekind reals}
\label{sec:algebr-struct-dedek}

The construction of the algebraic and order-theoretic structure of Dedekind reals proceeds
as usual in intuitionistic logic. Rather than dwelling on details we point out the
differences between the classical\index{mathematics!classical} and intuitionistic setup. Writing $L_x$ and $U_x$ for
the lower and upper cut of a real number $x : \RD$, we define addition as%
%
\indexdef{addition!of Dedekind reals}%
\begin{align*}
  L_{x + y}(q) &\defeq \exis{r, s : \Q} L_x(r) \land L_y(s) \land q = r + s, \\
  U_{x + y}(q) &\defeq \exis{r, s : \Q} U_x(r) \land U_y(s) \land q = r + s,
\end{align*}
%
and the additive inverse by
%
\begin{align*}
  L_{-x}(q) &\defeq \exis{r : \Q} U_x(r) \land q = - r, \\
  U_{-x}(q) &\defeq \exis{r : \Q} L_x(r) \land q = - r.
\end{align*}
%
With these operations $(\RD, 0, {+}, {-})$ is an abelian\index{group!abelian} group. Multiplication is a bit
more cumbersome:
%
\indexdef{multiplication!of Dedekind reals}%
\begin{align*}
  L_{x \cdot y}(q) &\defeq
  \begin{aligned}[t]
    \exis{a, b, c, d : \Q} & L_x(a) \land U_x(b) \land L_y(c) \land U_y(d) \land {}\\
                           & \qquad q < \min (a \cdot c, a \cdot d, b \cdot c, b \cdot d),
  \end{aligned} \\
  U_{x \cdot y}(q) &\defeq
  \begin{aligned}[t]
    \exis{a, b, c, d : \Q} & L_x(a) \land U_x(b) \land L_y(c) \land U_y(d) \land {}\\
                           & \qquad \max (a \cdot c, a \cdot d, b \cdot c, b \cdot d) < q.
  \end{aligned}
\end{align*}
%
\index{interval!arithmetic}%
These formulas are related to multiplication of intervals in interval arithmetic, where
intervals $[a,b]$ and $[c,d]$ with rational endpoints multiply to the interval
%
\begin{equation*}
  [a,b] \cdot [c,d] =
  [\min(a c, a d, b c, b d), \max(a c, a d, b c, b d)].
\end{equation*}
%
For instance, the formula for the lower cut can be read as saying that $q < x \cdot y$
when there are intervals $[a,b]$ and $[c,d]$ containing $x$ and $y$, respectively, such
that $q$ is to the left of $[a,b] \cdot [c,d]$. It is generally useful to think of an
interval $[a,b]$ such that $L_x(a)$ and $U_x(b)$ as an approximation of~$x$, see
\cref{ex:RD-interval-arithmetic}.

We now have a commutative ring\index{ring} with unit
\index{unit!of a ring}%
$(\RD, 0, 1, {+}, {-}, {\cdot})$. To treat
multiplicative inverses, we must first introduce order. Define $\leq$ and $<$ as
%
\begin{align*}
  (x \leq y) &\ \defeq \ \fall{q : \Q} L_x(q) \Rightarrow L_y(q), \\
  (x < y)    &\ \defeq \ \exis{q : \Q} U_x(q) \land L_y(q).
\end{align*}

\begin{lem} \label{dedekind-in-cut-as-le}
  For all $x : \RD$ and $q : \Q$, $L_x(q) \Leftrightarrow (q < x)$ and $U_x(q)
  \Leftrightarrow (x < q)$.
\end{lem}

\begin{proof}
  If $L_x(q)$ then by roundedness there merely is $r > q$ such that $L_x(r)$, and since
  $U_q(r)$ it follows that $q < x$. Conversely, if $q < x$ then there is $r : \Q$ such
  that $U_q(r)$ and $L_x(r)$, hence $L_x(q)$ because $L_x$ is a lower set. The other half
  of the proof is symmetric.
\end{proof}

\index{partial order}%
\index{transitivity!of . for reals@of $<$ for reals}
\index{transitivity!of . for reals@of $\leq$ for reals}
\index{relation!irreflexive}
\index{irreflexivity!of . for reals@of $<$ for reals}
The relation $\leq$ is a partial order, and $<$ is transitive and irreflexive. Linearity
\index{order!linear}%
\index{linear order}%
%
\begin{equation*}
  (x < y) \lor (y \leq x)
\end{equation*}
%
is valid if we assume excluded middle, but without it we get weak linearity
%
\index{order!weakly linear}
\index{weakly linear order}
\begin{equation} \label{eq:RD-linear-order}
  (x < y) \Rightarrow (x < z) \lor (z < y).
\end{equation}
%
At first sight it might not be clear what~\eqref{eq:RD-linear-order} has to do with
linear order. But if we take $x \jdeq u - \epsilon$ and $y \jdeq u + \epsilon$ for
$\epsilon > 0$, then we get
%
\begin{equation*}
  (u - \epsilon < z) \lor (z < u + \epsilon).
\end{equation*}
%
This is linearity ``up to a small numerical error'', i.e., since it is unreasonable to
expect that we can actually compute with infinite precision, we should not be surprised
that we can decide~$<$ only up to whatever finite precision we have computed.

To see that~\eqref{eq:RD-linear-order} holds, suppose $x < y$. Then there merely exists $q : \Q$ such that $U_x(q)$ and
$L_y(q)$. By roundedness there merely exist $r, s : \Q$ such that $r < q < s$, $U_x(r)$
and $L_y(s)$. Then, by locatedness $L_z(r)$ or $U_z(s)$. In the first case we get $x < z$
and in the second $z < y$.

Classically, multiplicative inverses exist for all numbers which are different from zero.
However, without excluded middle, a stronger condition is required. Say that $x, y : \RD$
are \define{apart}
\indexdef{apartness}%
from each other, written $x \apart y$, when $(x < y) \lor (y < x)$:
%
\symlabel{apart}
\begin{equation*}
  (x \apart y) \defeq (x < y) \lor (y < x).
\end{equation*}
%
If $x \apart y$, then $\lnot (x = y)$.
The converse is true if we assume excluded middle, but is not provable constructively.
\index{mathematics!constructive}%
Indeed, if $\lnot (x = y)$ implies $x\apart y$, then a little bit of excluded middle follows; see \cref{ex:reals-apart-neq-MP}.

\begin{thm} \label{RD-inverse-apart-0}
  A real is invertible if, and only if, it is apart from $0$.
\end{thm}

\begin{rmk}
  We observe that a real is invertible if, and only if, it is merely
  invertible.  Indeed, the same is true in any ring,\index{ring} since a ring is a set, and
  multiplicative inverses are unique if they exist.  See the discussion
  following \cref{cor:UC}.
\end{rmk}

\begin{proof}
  Suppose $x \cdot y = 1$. Then there merely exist $a, b, c, d : \Q$ such that
  $a < x < b$, $c < y < d$ and $0 < \min (a c, a d, b c, b d)$. From $0 < a c$ and $0 < b c$ it follows
  that $a$, $b$, and $c$ are either all positive or all negative.
  Hence either $0 < a < x$ or $x < b < 0$, so that $x \apart 0$.

  Conversely, if $x \apart 0$ then
  %
  \begin{align*}
    L_{x^{-1}}(q) &\defeq
    \exis{r : \Q} U_x(r) \land ((0 < r \land q r < 1) \lor (r < 0 \land 1 < q r))
    \\
    U_{x^{-1}}(q) &\defeq
    \exis{r : \Q} L_x(r) \land ((0 < r \land q r > 1) \lor (r < 0 \land 1 > q r))
  \end{align*}
  %
  defines the desired inverse. Indeed, $L_{x^{-1}}$ and $U_{x^{-1}}$ are inhabited because
  $x \apart 0$.
\end{proof}

\index{ordered field!archimedean}%
\index{dense}%
\indexsee{order-dense}{dense}%
The archimedean principle can be stated in several ways. We find it most illuminating in the
form which says that $\Q$ is dense in $\RD$.

\begin{thm}[Archimedean principle for $\RD$] \label{RD-archimedean}
  %
  For all $x, y : \RD$ if $x < y$ then there merely exists $q : \Q$ such that
  $x < q < y$.
\end{thm}

\begin{proof}
  By definition of $<$.
\end{proof}

Before tackling completeness of Dedekind reals, let us state precisely what algebraic
structure they possess. In the following definition we are not aiming at a minimal
axiomatization, but rather at a useful amount of structure and properties.

\begin{defn} \label{ordered-field} An \define{ordered field}
  \indexdef{ordered field}%
  \indexsee{field!ordered}{ordered field}%
  is a set $F$ together with
  constants $0$, $1$, operations $+$, $-$, $\cdot$, $\min$, $\max$, and mere relations
  $\leq$, $<$, $\apart$ such that:
  %
  \begin{enumerate}
  \item $(F, 0, 1, {+}, {-}, {\cdot})$ is a commutative ring with unit;
    \index{unit!of a ring}%
    \index{ring}%
  \item $x : F$ is invertible if, and only if, $x \apart 0$;
  \item $(F, {\leq}, {\min}, {\max})$ is a lattice;
  \item the strict order $<$ is transitive, irreflexive,
    \index{relation!irreflexive}
    \index{irreflexivity!of . in a field@of $<$ in a field}%
    and weakly linear ($x < y \Rightarrow x < z \lor z < y$);\index{transitivity!of . in a field@of $<$ in a field}
    \index{order!weakly linear}
    \index{weakly linear order}
    \index{strict!order}%
    \index{order!strict}%
  \item apartness $\apart$ is irreflexive, symmetric and cotransitive ($x \apart y \Rightarrow x \apart z \lor y \apart z$);
    \index{relation!irreflexive}
    \index{irreflexivity!of apartness}%
    \indexdef{relation!cotransitive}%
    \index{cotransitivity of apartness}%
  \item for all $x, y, z : F$:
    %
    \begin{align*}
      x \leq y &\Leftrightarrow \lnot (y < x), &
      x < y \leq z &\Rightarrow x < z, \\
      x \apart y &\Leftrightarrow (x < y) \lor (y < x), &
      x \leq y < z &\Rightarrow x < z, \\
      x \leq y &\Leftrightarrow x + z \leq y + z, &
      x \leq y \land 0 \leq z &\Rightarrow x z \leq y z, \\
      x < y &\Leftrightarrow x + z < y + z, &
      0 < z \Rightarrow (x < y &\Leftrightarrow x z < y z), \\
      0 < x + y &\Rightarrow 0 < x \lor 0 < y, &
      0 &< 1.
    \end{align*}
  \end{enumerate}
  %
  Every such field has a canonical embedding $\Q \to F$. An ordered field is
  \define{archimedean}
  \indexdef{ordered field!archimedean}%
  \indexsee{archimedean property}{ordered field, archi\-mede\-an}%
  when for all $x, y : F$, if $x < y$ then there merely exists $q :
  \Q$ such that $x < q < y$.
\end{defn}

\begin{thm} \label{RD-archimedean-ordered-field}
  The Dedekind reals form an ordered archimedean field.
\end{thm}

\begin{proof}
  We omit the proof in the hope that what we have demonstrated so far makes the theorem
  plausible.
\end{proof}

\subsection{Dedekind reals are Cauchy complete}
\label{sec:RD-cauchy-complete}

Recall that $x : \N \to \Q$ is a \emph{Cauchy sequence}\indexdef{Cauchy!sequence} when it satisfies
%
\begin{equation} \label{eq:cauchy-sequence}
  \prd{\epsilon : \Qp} \sm{n : \N} \prd{m, k \geq n} |x_m - x_k| < \epsilon.
\end{equation}
%
Note that we did \emph{not} truncate the inner existential because we actually want to
compute rates of convergence---an approximation without an error estimate carries little
useful information. By \cref{thm:ttac}, \eqref{eq:cauchy-sequence} yields a function $M
: \Qp \to \N$, called the \emph{modulus of convergence}\indexdef{modulus!of convergence}, such that $m, k \geq M(\epsilon)$
implies $|x_m - x_k| < \epsilon$. From this we get $|x_{M(\delta/2)} - x_{M(\epsilon/2)}|<
\delta + \epsilon$ for all $\delta, \epsilon : \Qp$. In fact, the map $(\epsilon \mapsto
x_{M(\epsilon/2)}) : \Qp \to \Q$ carries the same information about the limit as the
original Cauchy condition~\eqref{eq:cauchy-sequence}. We shall work with these
approximation functions rather than with Cauchy sequences.

\begin{defn} \label{defn:cauchy-approximation}
  A \define{Cauchy approximation}
  \indexdef{Cauchy!approximation}%
  is a map $x : \Qp \to \RD$ which satisfies
  %
  \begin{equation}
    \label{eq:cauchy-approx}
    \fall{\delta, \epsilon :\Qp} |x_\delta - x_\epsilon| < \delta + \epsilon.
  \end{equation}
  %
  The \define{limit}
  \index{limit!of a Cauchy approximation}%
  of a Cauchy approximation $x : \Qp \to \RD$ is a number $\ell : \RD$ such
  that
  %
  \begin{equation*}
    \fall{\epsilon, \theta : \Qp} |x_\epsilon - \ell| < \epsilon + \theta.
  \end{equation*}
\end{defn}

\begin{thm} \label{RD-cauchy-complete}
  Every Cauchy approximation in $\RD$ has a limit.
\end{thm}

\begin{proof}
  Note that we are showing existence, not mere existence, of the limit.
  Given a Cauchy approximation $x : \Qp \to \RD$, define
  %
  \begin{align*}
    L_y(q) &\defeq \exis{\epsilon, \theta : \Qp} L_{x_\epsilon}(q + \epsilon + \theta),\\
    U_y(q) &\defeq \exis{\epsilon, \theta : \Qp} U_{x_\epsilon}(q - \epsilon - \theta).
  \end{align*}
  %
  It is clear that $L_y$ and $U_y$ are inhabited, rounded, and disjoint. To establish
  locatedness, consider any $q, r : \Q$ such that $q < r$. There is $\epsilon : \Qp$ such
  that $5 \epsilon < r - q$. Since $q + 2 \epsilon < r - 2 \epsilon$ merely
  $L_{x_\epsilon}(q + 2 \epsilon)$ or $U_{x_\epsilon}(r - 2 \epsilon)$. In the first case
  we have $L_y(q)$ and in the second $U_y(r)$.

  To show that $y$ is the limit of $x$, consider any $\epsilon, \theta : \Qp$. Because
  $\Q$ is dense in $\RD$ there merely exist $q, r : \Q$ such that
  %
  \begin{narrowmultline*}
    x_\epsilon - \epsilon - \theta/2 < q < x_\epsilon - \epsilon - \theta/4
    < x_\epsilon < \\
    x_\epsilon + \epsilon + \theta/4 < r < x_\epsilon + \epsilon + \theta/2,
  \end{narrowmultline*}
  %
  and thus $q < y < r$. Now either $y < x_\epsilon + \theta/2$ or $x_\epsilon - \theta/2 < y$.
  In the first case we have
  %
  \begin{equation*}
    x_\epsilon - \epsilon - \theta/2 < q < y < x_\epsilon + \theta/2,
  \end{equation*}
  %
  and in the second
  %
  \begin{equation*}
    x_\epsilon - \theta/2 < y < r < x_\epsilon + \epsilon + \theta/2.
  \end{equation*}
  %
  In either case it follows that $|y - x_\epsilon| < \epsilon + \theta$.
\end{proof}

For sake of completeness we record the classic formulation as well.

\begin{cor}
  Suppose $x : \N \to \RD$ satisfies the Cauchy condition~\eqref{eq:cauchy-sequence}. Then
  there exists $y : \RD$ such that
  %
  \begin{equation*}
    \prd{\epsilon : \Qp} \sm{n : \N} \prd{m \geq n} |x_m - y| < \epsilon.
  \end{equation*}
\end{cor}

\begin{proof}
  By \cref{thm:ttac} there is $M : \Qp \to \N$ such that $\bar{x}(\epsilon) \defeq
  x_{M(\epsilon/2)}$ is a Cauchy approximation. Let $y$ be its limit, which exists by
  \cref{RD-cauchy-complete}. Given any $\epsilon : \Qp$, let $n \defeq M(\epsilon/4)$
  and observe that, for any $m \geq n$,
  %
  \begin{narrowmultline*}
    |x_m - y| \leq |x_m - x_n| + |x_n - y| =
    |x_m - x_n| + |\bar{x}(\epsilon/2) - y| < \narrowbreak
    \epsilon/4 + \epsilon/2 + \epsilon/4 = \epsilon.\qedhere
  \end{narrowmultline*}
\end{proof}

\subsection{Dedekind reals are Dedekind complete}
\label{sec:RD-dedekind-complete}

We obtained $\RD$ as the type of Dedekind cuts on $\Q$. But we could have instead started
with any archimedean ordered field $F$ and constructed Dedekind cuts\index{cut!Dedekind} on $F$. These would
again form an archimedean ordered field $\bar{F}$, the \define{Dedekind completion of $F$},%
\index{completion!Dedekind}%
\indexsee{Dedekind!completion}{completion, Dedekind}
with $F$ contained as a subfield. What happens if we apply this construction to
$\RD$, do we get even more real numbers? The answer is negative. In fact, we shall prove a
stronger result: $\RD$ is final.

Say that an ordered field~$F$ is \define{admissible for $\Omega$}
\indexsee{admissible!ordered field}{ordered field, admissible}%
\indexdef{ordered field!admissible}%
when the strict order
$<$ on~$F$ is a map ${<} : F \to F \to \Omega$.

\begin{thm} \label{RD-final-field}
  Every archimedean ordered field which is admissible for $\Omega$ is a subfield of~$\RD$.
\end{thm}

\begin{proof}
  Let $F$ be an archimedean ordered field. For every $x : F$ define $L_x, U_x : \Q \to
  \Omega$ by
  %
  \begin{equation*}
    L_x(q) \defeq (q < x)
    \qquad\text{and}\qquad
    U_x(q) \defeq (x < q).
  \end{equation*}
  %
  (We have just used the assumption that $F$ is admissible for $\Omega$.)
  Then $(L_x, U_x)$ is a Dedekind cut.\index{cut!Dedekind} Indeed, the cuts are inhabited and rounded because
  $F$ is archimedean and $<$ is transitive, disjoint because $<$ is irreflexive, and
  located because $<$ is a weak linear order. Let $e : F \to \RD$ be the map $e(x) \defeq (L_x,
  U_x)$.

  We claim that $e$ is a field embedding which preserves and reflects the order. First of
  all, notice that $e(q) = q$ for a rational number $q$. Next we have the equivalences,
  for all $x, y : F$,
  %
  \begin{narrowmultline*}
    x < y \Leftrightarrow
    (\exis{q : \Q} x < q < y) \Leftrightarrow \narrowbreak
    (\exis{q : \Q} U_x(q) \land L_y(q)) \Leftrightarrow
    e(x) < e(y),
  \end{narrowmultline*}
  %
  so $e$ indeed preserves and reflects the order. That $e(x + y) = e(x) + e(y)$ holds
  because, for all $q : \Q$,
  %
  \begin{equation*}
    q < x + y \Leftrightarrow
    \exis{r, s : \Q} r < x \land s < y \land q = r + s.
  \end{equation*}
  %
  The implication from right to left is obvious. For the other direction, if $q < x +
  y$ then there merely exists $r : \Q$ such that $q - y < r < x$, and by taking $s \defeq
  q - r$ we get the desired $r$ and $s$. We leave preservation of multiplication by $e$ as
  an exercise.
\end{proof}

To establish that the Dedekind cuts on $\RD$ do not give us anything new, we need just one
more lemma.

\begin{lem} \label{lem:cuts-preserve-admissibility}
  If $F$ is admissible for $\Omega$ then so is its Dedekind completion.
  \index{completion!Dedekind}%
\end{lem}

\begin{proof}
  Let $\bar{F}$ be the Dedekind completion of $F$. The strict order on $\bar{F}$ is
  defined by
  %
  \begin{equation*}
    ((L,U) < (L',U')) \defeq \exis{q : \Q} U(q) \land L'(q).
  \end{equation*}
  %
  Since $U(q)$ and $L'(q)$ are elements of $\Omega$, the lemma holds as long as $\Omega$
  is closed under conjunctions and countable existentials, which we assumed from the outset.
\end{proof}


\begin{cor} \label{RD-dedekind-complete}
  %
  \indexdef{complete!ordered field, Dedekind}%
  \indexdef{Dedekind!completeness}%
  The Dedekind reals are Dedekind complete: for every real-valued Dedekind cut $(L, U)$
  there is a unique $x : \RD$ such that $L(y) = (y < x)$ and $U(y) = (x < y)$ for all $y :
  \RD$.
\end{cor}

\begin{proof}
  By \cref{lem:cuts-preserve-admissibility} the Dedekind completion $\barRD$ of $\RD$
  is admissible for $\Omega$, so by \cref{RD-final-field} we have an embedding $\barRD
  \to \RD$, as well as an embedding $\RD \to \barRD$. But these embeddings must be
  isomorphisms, because their compositions are order-preserving field homomorphisms\index{homomorphism!field} which
  fix the dense subfield~$\Q$, which means that they are the identity. The corollary now
  follows immediately from the fact that $\barRD \to \RD$ is an isomorphism.
\end{proof}

\index{real numbers!Dedekind|)}%

\section{Cauchy reals}
\label{sec:cauchy-reals}

\index{real numbers!Cauchy|(}%
\index{completion!Cauchy|(}%
\indexsee{Cauchy!completion}{completion, Cauchy}%
The Cauchy reals are, by intent, the completion of \Q under limits of Cauchy sequences.\index{Cauchy!sequence}
In the classical construction of the Cauchy reals, we consider the set $\mathcal{C}$ of all Cauchy sequences in \Q and then form a suitable quotient $\mathcal{C}/{\approx}$.
Then, to show that $\mathcal{C}/{\approx}$ is Cauchy complete, we consider a Cauchy sequence $x : \N \to \mathcal{C}/{\approx}$, lift it to a sequence of sequences $\bar{x} : \N \to \mathcal{C}$, and construct the limit of $x$ using $\bar{x}$. However, the lifting of~$x$ to $\bar{x}$ uses
the axiom of countable choice (the instance of~\eqref{eq:ac} where $X=\N$) or the law of excluded middle, which we may wish to avoid.
\indexdef{axiom!of choice!countable}%
Every construction of reals whose last step is a quotient suffers from this deficiency.
There are three common ways out of the conundrum in constructive mathematics:
\index{mathematics!constructive}%
%
\index{bargaining}%
\begin{enumerate}
\item Pretend that the reals are a setoid $(\mathcal{C}, {\approx})$, i.e., the type of
  Cauchy sequences $\mathcal{C}$ with a coincidence\index{coincidence, of Cauchy approximations} relation attached to it by
  administrative decree. A sequence of reals then simply \emph{is} a sequence of Cauchy
  sequences representing them.
\item Give in to temptation and accept the axiom of countable choice. After all, the axiom
  is valid in most models of constructive mathematics based on a computational viewpoint,
  such as realizability models.
\item Declare the Cauchy reals unworthy and construct the Dedekind reals instead.
  Such a verdict is perfectly valid in certain contexts, such as in sheaf-theoretic models of constructive mathematics.
  However, as we saw in \cref{sec:dedekind-reals}, the constructive Dedekind reals have their own problems.
\end{enumerate}

Using higher inductive types, however, there is a fourth solution, which we believe to be preferable to any of the above, and interesting even to a classical mathematician.
The idea is that the Cauchy real numbers should be the \emph{free complete metric space}\index{free!complete metric space} generated by~\Q.
In general, the construction of a free gadget of any sort requires applying the gadget operations repeatedly many times to the generators.
For instance, the elements of the free group on a set $X$ are not just binary products and inverses of elements of $X$, but words obtained by iterating the product and inverse constructions.
Thus, we might naturally expect the same to be true for Cauchy completion, with the relevant ``operation'' being ``take the limit of a Cauchy sequence''.
(In this case, the iteration would have to take place transfinitely, since even after infinitely many steps there will be new Cauchy sequences to take the limit of.)

The argument referred to above shows that if excluded middle or countable choice hold, then Cauchy completion is very special: when building the completion of a space, it suffices to stop applying the operation after \emph{one step}.
This may be regarded as analogous to the fact that free monoids and free groups can be given explicit descriptions in terms of (reduced) words.
However, we saw in \cref{sec:free-algebras} that higher inductive types allow us to construct free gadgets \emph{directly}, whether or not there is also an explicit description available.
In this section we show that the same is true for the Cauchy reals (a similar technique would construct the Cauchy completion of any metric space; see \cref{ex:metric-completion}).
Specifically, higher inductive types allow us to \emph{simultaneously} add limits of Cauchy sequences and quotient by the coincidence relation, so that we can avoid the problem of lifting a sequence of reals to a sequence of representatives.
\index{completion!Cauchy|)}%


\subsection{Construction of Cauchy reals}
\label{sec:constr-cauchy-reals}

The construction of the Cauchy reals $\RC$ as a higher inductive type is a bit more subtle than that of the free algebraic structures considered in \cref{sec:free-algebras}.
We intend to include a ``take the limit'' constructor whose input is a Cauchy sequence of reals, but the notion of ``Cauchy sequence of reals'' depends on having some way to measure the ``distance'' between real numbers.
In general, of course, the distance between two real numbers will be another real number, leading to a potentially problematic circularity.

However, what we actually need for the notion of Cauchy sequence of reals is not the general notion of ``distance'', but a way to say that ``the distance\index{distance} between two real numbers is less than $\epsilon$'' for any $\epsilon:\Qp$.
This can be represented by a family of binary relations, which we will denote $\mathord{\close\epsilon} : \RC\to\RC\to \prop$.
The intended meaning of $x \close\epsilon y$ is $|x - y| < \epsilon$, but since we do not have notions of subtraction, absolute value, or inequality available yet (we are only just defining $\RC$, after all), we will have to define these relations $\close\epsilon$ at the same time as we define $\RC$ itself.
And since $\close\epsilon$ is a type family indexed by two copies of $\RC$, we cannot do this with an ordinary mutual (higher) inductive definition; instead we have to use a \emph{higher inductive-inductive definition}.
\index{inductive-inductive type!higher}

Recall from \cref{sec:generalizations} that the ordinary notion of inductive-inductive definition allows us to define a type and a type family indexed by it by simultaneous induction.
Of course, the ``higher'' version of this allows both the type and the family to have path constructors as well as point constructors.
We will not attempt to formulate any general theory of higher inductive-inductive definitions, but hopefully the description we will give of $\RC$ and $\close\epsilon$ will make the idea transparent.

\begin{rmk}
  We might also consider a \emph{higher inductive-recursive definition}, in which $\close\epsilon$ is defined using the \emph{recursion} principle of $\RC$, simultaneously with the \emph{inductive} definition of $\RC$.
  We choose the inductive-inductive route instead for two reasons.
  Firstly, higher inductive-re\-cur\-sive definitions seem to be more difficult to justify in homotopical semantics.
  Secondly, and more importantly, the inductive-inductive definition yields a more powerful induction principle, which we will need in order to develop even the basic theory of Cauchy reals.
\end{rmk}

Finally, as we did for the discussion of Cauchy completeness of the Dedekind reals in \cref{sec:RD-cauchy-complete}, we will work with \emph{Cauchy approximations} (\cref{defn:cauchy-approximation}) instead of Cauchy sequences.
Of course, our Cauchy approximations will now consist of Cauchy reals, rather than Dedekind reals or rational numbers.

\begin{defn}\label{defn:cauchy-reals}
  Let $\RC$ and the relation $\closesym:\Qp \times \RC \times \RC \to \type$ be the following higher inductive-inductive type family.
  The type $\RC$ of \define{Cauchy reals}
  \indexdef{real numbers!Cauchy}%
  \indexsee{Cauchy!real numbers}{real numbers, Cau\-chy}%
  is generated by the following constructors:
  \begin{itemize}
  \item \emph{rational points:}
    for any $q : \Q$ there is a real $\rcrat(q)$.
    \index{rational numbers!as Cauchy real numbers}%
  \item \emph{limit points}:
    for any $x : \Qp \to \RC$ such that
    %
    \begin{equation}
      \label{eq:RC-cauchy}
      \fall{\delta, \epsilon : \Qp} x_\delta \close{\delta + \epsilon} x_\epsilon
    \end{equation}
    %
    there is a point $\rclim(x) : \RC$. We call $x$ a \define{Cauchy approximation}.
    \indexdef{Cauchy!approximation}%
    \index{limit!of a Cauchy approximation}%
    %
  \item \emph{paths:}
    for $u, v : \RC$ such that
    %
    \begin{equation}
      \label{eq:RC-path}
      \fall{\epsilon : \Qp} u \close\epsilon v
    \end{equation}
    %
    then there is a path $\rceq(u, v) : \id[\RC]{u}{v}$.
  \end{itemize}
  Simultaneously, the type family $\closesym:\RC\to\RC\to\Qp \to\type$ is generated by the following constructors.
  Here $q$ and $r$ denote rational numbers; $\delta$, $\epsilon$, and $\eta$ denote positive rationals; $u$ and $v$ denote Cauchy reals; and $x$ and $y$ denote Cauchy approximations:
  \begin{itemize}
  \item for any $q,r,\epsilon$, if $-\epsilon < q - r < \epsilon$, then $\rcrat(q) \close\epsilon \rcrat(r)$,
  \item for any $q,y,\epsilon,\delta$, if $\rcrat(q) \close{\epsilon - \delta} y_\delta$, then $\rcrat(q) \close{\epsilon} \rclim(y)$,
  \item for any $x,r,\epsilon,\delta$, if $x_\delta \close{\epsilon - \delta} \rcrat(r)$, then $\rclim(x) \close\epsilon \rcrat(r)$,
  \item for any $x,y,\epsilon,\delta,\eta$, if $x_\delta \close{\epsilon - \delta - \eta} y_\eta$, then $\rclim(x) \close\epsilon \rclim(y)$,
  \item for any $u,v,\epsilon$, if $\xi,\zeta : u \close{\epsilon} v$, then $\xi=\zeta$ (propositional truncation).
  \end{itemize}
\end{defn}

\mentalpause

The first constructor of $\RC$ says that any rational number can be regarded as a real number.
The second says that from any Cauchy approximation to a real number, we can obtain a new real number called its ``limit''.
And the third expresses the idea that if two Cauchy approximations coincide, then their limits are equal.

The first four constructors of $\closesym$ specify when two rational numbers are close, when a rational is close to a limit, and when two limits are close.
In the case of two rational numbers, this is just the usual notion of $\epsilon$-closeness for rational numbers, whereas the other cases can be derived by noting that each approximant $x_\delta$ is supposed to be within $\delta$ of the limit $\rclim(x)$.

We remind ourselves of proof-relevance: a real number obtained from $\rclim$ is represented not
just by a Cauchy approximation $x$, but also a proof $p$ of~\eqref{eq:RC-cauchy}, so we
should technically have written $\rclim(x,p)$ instead of just $\rclim(x)$.
A similar observation also applies to $\rceq$ and~\eqref{eq:RC-path}, but we shall write just
$\rceq : u = v$ instead of $\rceq(u, v, p) : u = v$. These abuses of notation are
mitigated by the fact that we are omitting mere propositions and information that is
readily guessed.
Likewise, the last constructor of $\mathord{\close\epsilon}$ justifies our leaving the other four nameless.

We are immediately able to populate $\RC$ with many real numbers. For suppose $x : \N \to
\Q$ is a traditional Cauchy sequence\index{Cauchy!sequence} of rational numbers, and let $M : \Qp \to \N$ be its
modulus of convergence. Then $\rcrat \circ x \circ M : \Qp \to \RC$ is a Cauchy
approximation, using the first constructor of $\closesym$ to produce the necessary witness.
Thus, $\rclim(\rcrat \circ x \circ m)$ is a real number. Various famous
real numbers such as $\sqrt{2}$, $\pi$, $e$, \dots{} are all limits of such Cauchy sequences of
rationals.

\subsection{Induction and recursion on Cauchy reals}
\label{sec:induct-recurs-cauchy}

In order to do anything useful with $\RC$, of course, we need to give its induction principle.
As is the case whenever we inductively define two or more objects at once, the basic induction principle for $\RC$ and $\closesym$ requires a simultaneous induction over both at once.
Thus, we should expect it to say that assuming two type families over $\RC$ and $\closesym$, respectively, together with data corresponding to each constructor, there exist sections of both of these families.
However, since $\closesym$ is indexed on two copies of $\RC$, the precise dependencies of these families is a bit subtle.
The induction principle will apply to any pair of type families:
\begin{align*}
A&:\RC\to\type\\
B&:\prd{x,y:\RC} A(x) \to A(y) \to \prd{\epsilon:\Qp} (x\close\epsilon y) \to \type.
\end{align*}
The type of $A$ is obvious, but the type of $B$ requires a little thought.
Since $B$ must depend on $\closesym$, but $\closesym$ in turn depends on two copies of $\RC$ and one copy of $\Qp$, it is fairly obvious that $B$ must also depend on the variables $x,y:\RC$ and $\epsilon:\Qp$ as well as an element of $(x\close\epsilon y)$.
What is slightly less obvious is that $B$ must also depend on $A(x)$ and $A(y)$.

This may be more evident if we consider the non-dependent case (the recursion principle), where $A$ is a simple type (rather than a type family).
In this case we would expect $B$ not to depend on $x,y:\RC$ or $x\close\epsilon y$.
But the recursion principle (along with its associated uniqueness principle) is supposed to say that $\RC$ with $\close\epsilon$ is an ``initial object'' in some category, so in this case the dependency structure of $A$ and $B$ should mirror that of $\RC$ and $\close\epsilon$: that is, we should have $B:A\to A\to \Qp \to \type$.
Combining this observation with the fact that, in the dependent case, $B$ must also depend on $x,y:\RC$ and $x\close\epsilon y$, leads inevitably to the type given above for $B$.

\symlabel{RC-recursion}
It is helpful to think of $B$ as an $\epsilon$-indexed family of relations between the types $A(x)$ and $A(y)$.
With this in mind, we may write $B(x,y,a,b,\epsilon,\xi)$ as $(x,a) \bsim_\epsilon^\xi (y,b)$.
Since $\xi:x\close\epsilon y$ is unique when it exists, we generally omit it from the notation and write $(x,a) \bsim_\epsilon (y,b)$; this is harmless as long as we keep in mind that this relation is only defined when $x\close\epsilon y$.
We may also sometimes simplify further and write $a\bsim_\epsilon b$, with $x$ and $y$ inferred from the types of $a$ and $b$, but sometimes it will be necessary to include them for clarity.

\index{induction principle!for Cauchy reals}%
Now, given a type family $A:\RC\to\type$ and a family of relations $\bsim$ as above, the hypotheses of the induction principle consist of the following data, one for each constructor of $\RC$ or $\closesym$:
\begin{itemize}
\item For any $q : \Q$, an element $f_q:A(\rcrat(q))$.
\item For any Cauchy approximation $x$, and any $a:\prd{\epsilon:\Qp} A(x_\epsilon)$ such that
  \begin{equation}
    \fall{\delta, \epsilon : \Qp}
    (x_\delta,a_\delta) \bsim_{\delta+\epsilon} (x_\epsilon,a_\epsilon),
    \label{eq:depCauchyappx}
  \end{equation}
  an element $f_{x,a}:A(\rclim(x))$.
  We call such $a$ a \define{dependent Cauchy approximation}
  \indexdef{Cauchy!approximation!dependent}%
  \indexsee{approximation, Cauchy}{Cauchy approximation}%
  \indexdef{dependent!Cauchy approximation}%
  over $x$.
\item For $u, v : \RC$ such that $h:\fall{\epsilon : \Qp} u \close\epsilon v$, and all $a:A(u)$ and $b:A(v)$ such that
  $\fall{\epsilon:\Qp} (u,a) \bsim_\epsilon (v,b)$,
  a dependent path $\dpath{A}{\rceq(u,v)}{a}{b}$.
\item For $q,r:\Q$ and $\epsilon:\Qp$, if $-\epsilon < q - r < \epsilon$, we have
  \narrowequation{(\rcrat(q),f_q) \bsim_\epsilon (\rcrat(r),f_r).}
\item For $q:\Q$ and $\delta,\epsilon:\Qp$ and $y$ a Cauchy approximation, and $b$ a dependent Cauchy approximation over $y$, if $\rcrat(q) \close{\epsilon - \delta} y_\delta$, then
  \[(\rcrat(q),f_q) \bsim_{\epsilon-\delta} (y_\delta,b_\delta)
  \;\Rightarrow\;
  (\rcrat(q),f_q) \bsim_\epsilon (\rclim(y),f_{y,b}).\]
\item Similarly, for $r:\Q$ and $\delta,\epsilon:\Qp$ and $x$ a Cauchy approximation, and $a$ a dependent Cauchy approximation over $x$, if $x_\delta \close{\epsilon - \delta} \rcrat(r)$, then
  \[(x_\delta,a_\delta) \bsim_{\epsilon-\delta} (\rcrat(r),f_r)
  \;\Rightarrow\;
  (\rclim(x),f_{x,a}) \bsim_\epsilon (\rcrat(q),f_r).
  \]
\item For $\epsilon,\delta,\eta:\Qp$ and $x,y$ Cauchy approximations, and $a$ and $b$ dependent Cauchy approximations over $x$ and $y$ respectively, if we have $x_\delta \close{\epsilon - \delta - \eta} y_\eta$, then
  \[ (x_\delta,a_\delta) \bsim_{\epsilon - \delta - \eta} (y_\eta,b_\eta)
  \;\Rightarrow\;
  (\rclim(x),f_{x,a}) \bsim_\epsilon (\rclim(y),f_{y,b}).\]
\item For $\epsilon:\Qp$ and $x,y:\RC$ and $\xi,\zeta:x\close{\epsilon} y$, and $a:A(x)$ and $b:A(y)$, any two elements of $(x,a) \bsim_\epsilon^\xi (y,b)$ and $(x,a) \bsim_\epsilon^\zeta (y,b)$ are dependently equal over $\xi=\zeta$.
  Note that as usual, this is equivalent to asking that $\bsim$ takes values in mere propositions.
\end{itemize}
Under these hypotheses, we deduce functions
\begin{align*}
  f&:\prd{x:\RC} A(x)\\
  g&:\prd{x,y:\RC}{\epsilon:\Qp}{\xi:x\close{\epsilon} y}
  (x,f(x)) \bsim_\epsilon^\xi (y,f(y))
\end{align*}
which compute as expected:
\begin{align}
  f(\rcrat(q)) &\defeq f_q, \label{eq:rcsimind1}\\
  f(\rclim(x)) &\defeq f_{x,(f,g)[x]}. \label{eq:rcsimind2}
\end{align}
Here $(f,g)[x]$ denotes the result of applying $f$ and $g$ to a Cauchy approximation $x$ to obtain a dependent Cauchy approximation over $x$.
That is, we define $(f,g)[x]_\epsilon \defeq f(x_\epsilon) : A(x_\epsilon)$, and then for any $\epsilon,\delta:\Qp$ we have $g(x_\epsilon,x_\delta,\epsilon+\delta,\xi)$ to witness the fact that $(f,g)[x]$ is a dependent Cauchy approximation, where $\xi: x_\epsilon \close{\epsilon+\delta} x_\delta$ arises from the assumption that $x$ is a Cauchy approximation.

We will never use this notation again, so don't worry about remembering it.
Generally we use the pattern-matching convention, where $f$ is defined by equations such as~\eqref{eq:rcsimind1} and~\eqref{eq:rcsimind2} in which the right-hand side of~\eqref{eq:rcsimind2} may involve the symbols $f(x_\epsilon)$ and an assumption that they form a dependent Cauchy approximation.

However, this induction principle is admittedly still quite a mouthful.
To help make sense of it, we observe that it contains as special cases two separate induction principles for~$\RC$ and for~$\closesym$.
Firstly, suppose given only a type family $A:\RC\to\type$, and define $\bsim$ to be constant at \unit.
Then much of the required data becomes trivial, and we are left with:
\begin{itemize}
\item for any $q : \Q$, an element $f_q:A(\rcrat(q))$,
\item for any Cauchy approximation $x$, and any $a:\prd{\epsilon:\Qp} A(x_\epsilon)$, an element $f_{x,a}:A(\rclim(x))$,
\item for $u, v : \RC$ and $h:\fall{\epsilon : \Qp} u \close\epsilon v$, and $a:A(u)$ and $b:A(v)$, we have $\dpath{A}{\rceq(u,v)}{a}{b}$.
\end{itemize}
Given these data, the induction principle yields a function $f:\prd{x:\RC} A(x)$ such that
\begin{align*}
  f(\rcrat(q)) &\defeq f_q,\\
  f(\rclim(x)) &\defeq f_{x,f(x)}.
\end{align*}
We call this principle \define{$\RC$-induction}; it says essentially that if we take $\close\epsilon$ as given, then $\RC$ is inductively generated by its constructors.

Note that, if $A$ is a mere property, then the third hypothesis in $\RC$-induction is automatic (we will see in a moment that these are in fact equivalent statements).
Thus, we may prove mere properties of real numbers by simply proving them for rationals and for limits of Cauchy approximations.
Here is an example.

\begin{lem} \label{lem:close-reflexive}
  For any $u:\RC$ and $\epsilon:\Qp$, we have $u\close\epsilon u$.
\end{lem}
\begin{proof}
  Define $A(u) \defeq \fall{\epsilon:\Qp} (u\close\epsilon u)$.
  Since this is a mere proposition (by the last constructor of $\closesym$), by $\RC$-induction, it suffices to prove it when $u$ is $\rcrat(q)$ and when $u$ is $\rclim(x)$.
  In the first case, we obviously have $|q-q|<\epsilon$ for any $\epsilon$, hence $\rcrat(q) \close\epsilon \rcrat(q)$ by the first constructor of $\closesym$.
  %
  And in the second case, we may assume inductively that $x_\delta \close\epsilon x_\delta$ for all $\delta,\epsilon:\Qp$.
  Then in particular, we have $x_{\epsilon/3} \close{\epsilon/3} x_{\epsilon/3}$, whence $\rclim(x) \close{\epsilon} \rclim(x)$ by the fourth constructor of $\closesym$.
\end{proof}

From \cref{lem:close-reflexive}, we infer that a direct application of $\RC$-induction only has a chance to succeed if the family $A:\RC\to\type$ is a mere property.
To see this, fix $u:\RC$.
Taking $v$ to be $u$, the third hypothesis of $\RC$-induction tells us that, for any $a : A(u)$, we have $\dpath{A}{\rceq(u,u)}{a}{a}$.
Given a point $b : A(u)$ in addition, we also get $\dpath{A}{\rceq(u,u)}{a}{b}$.
From the definition of the dependent path type, we conclude that the combination of these two paths implies $a = b$, i.e.\ all points in $A(u)$ are equal.

\begin{thm}\label{thm:Cauchy-reals-are-a-set}
  $\RC$ is a set.
\end{thm}
\begin{proof}
  We have just shown that the mere relation
  \narrowequation{P(u,v) \defeq \fall{\epsilon:\Qp} (u\close\epsilon v)}
  is reflexive.
  Since it implies identity, by the path constructor of $\RC$, the result follows from \cref{thm:h-set-refrel-in-paths-sets}.
\end{proof}

We can also show that although $\RC$ may not be a quotient of the set of Cauchy sequences of \emph{rationals}, it is nevertheless a quotient of the set of Cauchy sequences of \emph{reals}.
(Of course, this is not a valid \emph{definition} of $\RC$, but it is a useful property.)
We define the type of Cauchy approximations to be
%
\symlabel{cauchy-approximations}%
\index{Cauchy!approximation!type of}%
\begin{equation*}
  \CAP \defeq
  \setof{ x : \Qp \to \RC |
    \fall{\epsilon, \delta : \Qp} x_\delta \close{\delta + \epsilon} x_\epsilon
  }.
\end{equation*}
The second constructor of $\RC$ gives a function $\rclim:\CAP\to\RC$.

\begin{lem} \label{RC-lim-onto}
  Every real merely is a limit point: $\fall{u : \RC} \exis{x : \CAP} u = \rclim(x)$.
  In other words, $\rclim:\CAP\to\RC$ is surjective.
\end{lem}
\begin{proof}
  By $\RC$-induction, we may divide into cases on $u$.
  Of course, if $u$ is a limit $\rclim(x)$, the statement is trivial.
  So suppose $u$ is a rational point $\rcrat(q)$; we claim $u$ is equal to $\rclim(\lam{\epsilon} \rcrat(q))$.
  By the path constructor of $\RC$, it suffices to show $\rcrat(q) \close\epsilon \rclim(\lam{\epsilon} \rcrat(q))$ for all $\epsilon:\Qp$.
  And by the second constructor of $\closesym$, for this it suffices to find $\delta:\Qp$ such that $\rcrat(q)\close{\epsilon-\delta} \rcrat(q)$.
  But by the first constructor of $\closesym$, we may take any $\delta:\Qp$ with $\delta<\epsilon$.
\end{proof}

%

\begin{lem} \label{RC-lim-factor}
  If $A$ is a set and $f : \CAP \to A$ respects coincidence\index{coincidence!of Cauchy approximations} of Cauchy approximations, in the sense that
  %
  \begin{equation*}
    \fall{x, y : \CAP} \rclim(x) = \rclim(y) \Rightarrow f(x) = f(y),
  \end{equation*}
  %
  then $f$ factors uniquely through $\rclim : \CAP \to \RC$.
\end{lem}
\begin{proof}
  Since $\rclim$ is surjective, by \cref{lem:images_are_coequalizers}, $\RC$ is the quotient of $\CAP$ by the kernel pair\index{kernel!pair} of $\rclim$.
  But this is exactly the statement of the lemma.
\end{proof}

For the second special case of the induction principle, suppose instead that we take $A$ to be constant at $\unit$.
In this case, $\bsim$ is simply an $\epsilon$-indexed family of relations on $\epsilon$-close pairs of real numbers, so we may write $u\bsim_\epsilon v$ instead of $(u,\ttt)\bsim_\epsilon (v,\ttt)$.
Then the required data reduces to the following, where $q, r$ denote rational numbers, $\epsilon, \delta, \eta$ positive rational numbers, and $x, y$ Cauchy approximations:
\begin{itemize}
\item if $-\epsilon < q - r < \epsilon$, then
  $\rcrat(q) \bsim_\epsilon \rcrat(r)$,
\item if $\rcrat(q) \close{\epsilon - \delta} y_\delta$ and
  $\rcrat(q)\bsim_{\epsilon-\delta} y_\delta$,
  then $\rcrat(q) \bsim_\epsilon \rclim(y)$,
\item if $x_\delta \close{\epsilon - \delta} \rcrat(r)$ and
  $x_\delta \bsim_{\epsilon-\delta} \rcrat(r)$,
  then $\rclim(y) \bsim_\epsilon \rcrat(q)$,
\item if $x_\delta \close{\epsilon - \delta - \eta} y_\eta$ and
  $x_\delta\bsim_{\epsilon - \delta - \eta} y_\eta$,
  then $\rclim(x) \bsim_\epsilon \rclim(y)$.
\end{itemize}
The resulting conclusion is $\fall{u,v:\RC}{\epsilon:\Qp} (u\close\epsilon v) \to (u \bsim_\epsilon v)$.
We call this principle \define{$\closesym$-induction}; it says essentially that if we take $\RC$ as given, then $\close\epsilon$ is inductively generated (as a family of types) by \emph{its} constructors.
For example, we can use this to show that $\closesym$ is symmetric.

\begin{lem}\label{thm:RCsim-symmetric}
  For any $u,v:\RC$ and $\epsilon:\Qp$, we have $(u\close\epsilon v) = (v\close\epsilon u)$.
\end{lem}
\begin{proof}
  Since both are mere propositions, by symmetry it suffices to show one implication.
  Thus, let $(u\bsim_\epsilon v) \defeq (v\close\epsilon u)$.
  By $\closesym$-induction, we may reduce to the case that $u\close\epsilon v$ is derived from one of the four interesting constructors of $\closesym$.
  In the first case when $u$ and $v$ are both rational, the result is trivial (we can apply the first constructor again).
  In the other three cases, the inductive hypothesis (together with commutativity of addition in $\Q$) yields exactly the input to another of the constructors of $\closesym$ (the second and third constructors switch, while the fourth stays put).
\end{proof}

The general induction principle, which we may call \define{$(\RC,\closesym)$-induction}, is therefore a sort of joint $\RC$-induction and $\closesym$-induction.
Consider, for instance, its non-dependent version, which we call \define{$(\RC,\closesym)$-recursion}, which is the one that we will have the most use for.
\index{recursion principle!for Cauchy reals}%
Ordinary $\RC$-recursion tells us that to define a function $f : \RC \to A$ it suffices to:
\begin{enumerate}
\item for every $q : \Q$ construct $f(\rcrat(q)) : A$,
\item for every Cauchy approximation $x : \Qp \to \RC$, construct $f(x) : A$,
  assuming that $f(x_\epsilon)$ has already been defined for all $\epsilon : \Qp$,
\item prove $f(u) = f(v)$ for all $u, v : \RC$ satisfying $\fall{\epsilon:\Qp} u\close\epsilon v$.\label{item:rcrec3}
\end{enumerate}
However, it is generally quite difficult to show~\ref{item:rcrec3} without knowing something about how $f$ acts on $\epsilon$-close Cauchy reals.
The enhanced principle of $(\RC,\closesym)$-recursion remedies this deficiency, allowing us to specify an \emph{arbitrary} ``way in which $f$ acts on $\epsilon$-close Cauchy reals'', which we can then prove to be the case by a simultaneous induction with the definition of $f$.
This is the family of relations $\bsim$.
Since $A$ is independent of $\RC$, we may assume for simplicity that $\bsim$ depends only on $A$ and $\Qp$, and thus there is no ambiguity in writing $a\bsim_\epsilon b$ instead of $(u,a) \bsim_\epsilon (v,b)$.
In this case, defining a function $f:\RC\to A$ by $(\RC,\closesym)$-recursion requires the following cases (which we now write using the pattern-matching convention).
\begin{itemize}
\item For every $q : \Q$, construct $f(\rcrat(q)) : A$.
\item For every Cauchy approximation $x : \Qp \to \RC$, construct $f(x) : A$, assuming inductively that $f(x_\epsilon)$ has already been defined for all $\epsilon : \Qp$ and form a ``Cauchy approximation with respect to $\bsim$'', i.e.\ that $\fall{\epsilon,\delta:\Qp} (f(x_\epsilon) \bsim_{\epsilon+\delta} f(x_\delta))$.
\item Prove that the relations $\bsim$ are \emph{separated}, i.e.\ that, for any $a,b:A$,
  \indexdef{relation!separated family of}%
  \indexdef{separated family of relations}%
\narrowequation{(\fall{\epsilon:\Qp} a\bsim_\epsilon b) \Rightarrow (a=b).}
\item Prove that if $-\epsilon< q-r <\epsilon$ for $q,r:\Q$, then $f(\rcrat(q))\bsim_\epsilon f(\rcrat(r))$.
\item For any $q:\Q$ and any Cauchy approximation $y$, prove that
\narrowequation{f(\rcrat(q)) \bsim_\epsilon f(\rclim(y)),} assuming inductively that $\rcrat(q)\close{\epsilon-\delta} y_\delta$ and $f(\rcrat(q)) \bsim_{\epsilon-\delta} f(y_\delta)$ for some $\delta:\Qp$, and that $\eta \mapsto f(x_\eta)$ is a Cauchy approximation with respect to $\bsim$.
\item For any Cauchy approximation $x$ and any $r:\Q$, prove that
\narrowequation{f(\rclim(x)) \bsim_\epsilon f(\rcrat(r)),}
assuming inductively that $x_\delta \close{\epsilon-\delta} \rcrat(r)$ and $f(x_\delta) \bsim_{\epsilon-\delta} f(\rcrat(r))$ for some $\delta:\Qp$, and that $\eta\mapsto f(x_\eta)$ is a Cauchy approximation with respect to $\bsim$.
\item For any Cauchy approximations $x,y$, prove that
\narrowequation{f(\rclim(x)) \bsim_\epsilon f(\rclim(y)),}
assuming inductively that $x_\delta \close{\epsilon-\delta-\eta} y_\eta$ and $f(x_\delta) \bsim_{\epsilon-\delta-\eta} f(y_\eta)$ for some $\delta,\eta:\Qp$, and that $\theta\mapsto f(x_\theta)$ and $\theta\mapsto f(y_\theta)$ are Cauchy approximations with respect to $\bsim$.
\end{itemize}
Note that in the last four proofs, we are free to use the specific definitions of $f(\rcrat(q))$ and $f(\rclim(x))$ given in the first two data.
However, the proof of separatedness must apply to \emph{any} two elements of $A$, without any relation to $f$: it is a sort of ``admissibility'' condition on the family of relations $\bsim$.
Thus, we often verify it first, immediately after defining $\bsim$, before going on to define $f(\rcrat(q))$ and $f(\rclim(x))$.

Under the above hypotheses, $(\RC,\closesym)$-recursion yields a function $f:\RC\to A$ such that $f(\rcrat(q))$ and $f(\rclim(x))$ are judgmentally equal to the definitions given for them in the first two clauses.
Moreover, we may also conclude
\begin{equation}
  \fall{u,v:\RC}{\epsilon:\Qp} (u\close\epsilon v) \to (f(u) \bsim_\epsilon f(v)).\label{eq:RC-sim-recursion-extra}
\end{equation}

As a paradigmatic example, $(\RC,\closesym)$-recursion allows us to extend functions defined on $\Q$ to all of $\RC$, as long as they are sufficiently continuous.
\index{function!continuous}%

\begin{defn}\label{defn:lipschitz}
  A function $f:\Q\to\RC$ is \define{Lipschitz}
  \indexdef{function!Lipschitz}%
  \indexdef{Lipschitz!function}%
  \indexdef{Lipschitz!constant}%
  \indexdef{constant!Lipschitz}%
  if there exists $L:\Qp$ (the \define{Lipschitz constant}) such that
  \[ |q - r|<\epsilon \Rightarrow (f(q) \close{L\epsilon} f(r)) \]
  for all $\epsilon:\Qp$ and $q,r:\Q$.
  %
  Similarly, $g:\RC\to\RC$ is \define{Lipschitz} if there exists $L:\Qp$ such that
  \[ (u\close\epsilon v) \Rightarrow (g(u) \close{L\epsilon} g(v)) \]
  for all $\epsilon:\Qp$ and $u,v:\RC$..
\end{defn}

In particular, note that by the first constructor of $\closesym$, if $f:\Q\to\Q$ is Lipschitz in the obvious sense, then so is the composite $\Q\xrightarrow{f} \Q \to \RC$.

\begin{lem}\label{RC-extend-Q-Lipschitz}
  Suppose $f : \Q \to \RC$ is Lipschitz with constant $L : \Qp$.
  Then there exists a Lipschitz map $\bar{f} : \RC \to \RC$, also with constant $L$, such that $\bar{f}(\rcrat(q)) \jdeq f(q)$ for all $q:\Q$.
\end{lem}

\begin{proof}
  % Uniqueness follows directly from \cref{RC-continuous-eq}.
  We define $\bar{f}$ by $(\RC,\closesym)$-recursion, with codomain $A\defeq \RC$.
  We define the relation $\mathord{\bsim}: \RC \to \RC \to \Qp \to \prop$ to be
  \begin{align*}
    (u \bsim_\epsilon v) &\defeq (u \close{L\epsilon} v).
  \end{align*}
  For $q : \Q$, we define
  %
  \begin{equation*}
    \bar{f}(\rcrat(q)) \defeq \rcrat(f(q)).
  \end{equation*}
  %
  For a Cauchy approximation $x : \Qp \to \RC$, we define
  %
  \begin{equation*}
    \bar{f}(\rclim(x)) \defeq \rclim(\lamu{\epsilon : \Qp} \bar{f}(x_{\epsilon/L})).
  \end{equation*}
  %
  For this to make sense, we must verify that $y \defeq \lamu{\epsilon : \Qp} \bar{f}(x_{\epsilon/L})$ is a Cauchy approximation.
  However, the inductive hypothesis for this step is that for any $\delta,\epsilon:\Qp$ we have $\bar{f}(x_\delta) \bsim_{\delta+\epsilon} \bar{f}(x_\epsilon)$, i.e.\ $\bar{f}(x_\delta) \close{L\delta+L\epsilon} \bar{f}(x_\epsilon)$.
  Thus we have
  \[y_\delta \jdeq f(x_{\delta/L}) \close{\delta + \epsilon} f(x_{\epsilon/L})   \jdeq y_\epsilon. \]

  For proving separatedness, we simply observe that $\fall{\epsilon:\Qp} a\bsim_\epsilon b$ means $\fall{\epsilon:\Qp} a\close{L\epsilon} b$, which implies $\fall{\epsilon:\Qp}a\close\epsilon b$ and thus $a=b$.

  To complete the $(\RC,\closesym)$-recursion, it remains to verify the four conditions on $\bsim$.
  This basically amounts to proving that $\bar f$ is Lipschitz for all the four constructors of $\closesym$.
  \begin{enumerate}
  \item When $u$ is $\rcrat(q)$ and $v$ is $\rcrat(r)$ with $-\epsilon < |q-r| <\epsilon$, the assumption that $f$ is Lipschitz yields $f(q) \close{L\epsilon} f(r)$, hence $\bar{f}(\rcrat(q)) \bsim_\epsilon \bar{f}(\rcrat(r))$ by definition.
  \item When $u$ is $\rclim(x)$ and $v$ is $\rcrat(q)$ with $x_\eta \close{\epsilon - \eta} \rcrat(q)$, then the
      inductive hypothesis is $\bar{f}(x_\eta) \close{L \epsilon - L \eta} \rcrat(f(q))$, which proves
      \narrowequation{\bar{f}(\rclim(x)) \close{L \epsilon} \bar{f}(\rcrat(q))}
      by the third constructor of $\closesym$.
  \item The symmetric case when $u$ is rational and $v$ is a limit is essentially identical.
  \item When $u$ is $\rclim(x)$ and $v$ is $\rclim(y)$, with $\delta, \eta : \Qp$ such that $x_\delta \close{\epsilon - \delta - \eta} y_\eta$,
      the inductive hypothesis is $\bar{f}(x_\delta) \close{L \epsilon - L \delta - L \eta} \bar{f}(y_\eta)$, which proves $\bar{f}(\rclim(x)) \close{L
        \epsilon} \bar{f}(\rclim(y))$ by the fourth constructor of $\closesym$.
  \end{enumerate}
  This completes the $(\RC,\closesym)$-recursion, and hence the construction of $\bar f$.
  The desired equality $\bar f(\rcrat(q))\jdeq f(q)$ is exactly the first computation rule for $(\RC,\closesym)$-recursion, and the additional condition~\eqref{eq:RC-sim-recursion-extra} says exactly that $\bar f$ is Lipschitz with constant $L$.
\end{proof}

At this point we have gone about as far as we can without a better characterization of $\closesym$.
We have specified, in the constructors of $\closesym$, the conditions under which we want Cauchy reals of the two different forms to be $\epsilon$-close.
However, how do we know that in the resulting inductive-inductive type family, these are the \emph{only} witnesses to this fact?
We have seen that inductive type families (such as identity types, see \cref{sec:identity-systems}) and higher inductive types have a tendency to contain ``more than was put into them'', so this is not an idle question.

In order to characterize $\closesym$ more precisely, we will define a family of relations $\approx_\epsilon$ on $\RC$ \emph{recursively}, so that they will compute on constructors, and prove that this family is equivalent to $\close\epsilon$.

\begin{thm}\label{defn:RC-approx}
  There is a family of mere relations $\mathord\approx:\RC\to\RC\to\Qp\to\prop$ such that
  \begin{align}
    (\rcrat(q) \approx_\epsilon \rcrat(r))  &\defeq
    (-\epsilon < q - r < \epsilon)\label{eq:RCappx1}\\
    (\rcrat(q) \approx_\epsilon \rclim(y)) &\defeq
    \exis{\delta : \Qp} \rcrat(q) \approx_{\epsilon - \delta} y_\delta\label{eq:RCappx2}\\
    (\rclim(x) \approx_\epsilon \rcrat(r)) &\defeq
    \exis{\delta : \Qp} x_\delta \approx_{\epsilon - \delta} \rcrat(r)\label{eq:RCappx3}\\
    (\rclim(x) \approx_\epsilon \rclim(y)) &\defeq
    \exis{\delta, \eta : \Qp} x_\delta \approx_{\epsilon - \delta - \eta} y_\eta.\label{eq:RCappx4}
  \end{align}
  Moreover, we have
  \begin{gather}
    (u \approx_\epsilon v) \Leftrightarrow \exis{\theta:\Qp} (u \approx_{\epsilon-\theta} v) \label{RC-sim-rounded}\\
    (u \approx_\epsilon v) \to (v\close\delta w) \to (u\approx_{\epsilon+\delta} w)\label{eq:RC-sim-rtri}\\
    (u \close\epsilon v) \to (v\approx_\delta w) \to (u\approx_{\epsilon+\delta} w)\label{eq:RC-sim-ltri}.
  \end{gather}
\end{thm}

The additional conditions~\eqref{RC-sim-rounded}--\eqref{eq:RC-sim-ltri} turn out to be required in order to make the inductive definition go through.
Condition~\eqref{RC-sim-rounded} is called being \define{rounded}.
\indexsee{relation!rounded}{rounded relation}%
\indexdef{rounded!relation}%
Reading it from right to left gives \define{monotonicity} of $\approx$,
\index{monotonicity}%
\index{relation!monotonic}%
%
\begin{equation*}
  (\delta < \epsilon) \land (u \approx_\delta v) \Rightarrow (u \approx_\epsilon v)
\end{equation*}
%
while reading it left to right to \define{openness} of $\approx$,
\index{open!relation}%
\index{relation!open}%
%
\begin{equation*}
  (u \approx_\epsilon v) \Rightarrow \exis{\delta : \Qp} (\delta < \epsilon) \land (u \approx_\delta v).
\end{equation*}
%
Conditions~\eqref{eq:RC-sim-rtri} and~\eqref{eq:RC-sim-ltri} are forms of the triangle inequality, which say that $\approx$ is a ``module'' over $\closesym$ on both sides.

\begin{proof}
  We will define $\mathord\approx:\RC\to\RC\to\Qp\to\prop$ by double $(\RC,\closesym)$-recursion.
  First we will apply $(\RC,\closesym)$-recursion with codomain the subset of $\RC\to\Qp\to\prop$ consisting of those families of predicates which are rounded and satisfy the one appropriate form of the triangle inequality.
  Thinking of these predicates as half of a binary relation, we will write them as $(u,\epsilon) \mapsto (\hapx_\epsilon u)$, with the symbol $\hapname$ referring to the whole relation.
  Now we can write $A$ precisely as
  \begin{multline*}
    A \defeq\; \Bigg\{ \hapname :\RC\to\Qp\to\prop \;\bigg|\; \\
    \Big(\fall{u:\RC}{\epsilon:\Qp}
    \big((\hapx_\epsilon u) \Leftrightarrow \exis{\theta:\Qp} (\hapx_{\epsilon-\theta} u)\big)\Big)  \\
    \land \Big(\fall{u,v:\RC}{\eta,\epsilon:\Qp} (u\close\epsilon v) \to\\
    \big((\hapx_\eta u) \to (\hapx_{\eta+\epsilon} v) \big) \land \big((\hapx_\eta v) \to (\hapx_{\eta+\epsilon} u) \big)\Big)\Bigg\}
  \end{multline*}
  As usual with subsets, we will use the same notation for an inhabitant of $A$ and its first component $\hapname$.
  As the family of relations required for $(\RC,\closesym)$-recursion, we consider the following, which will ensure the other form of the triangle inequality:
  \begin{narrowmultline*}
    (\hapname \bsim_\epsilon \hapbname ) \defeq \narrowbreak
    \fall{u:\RC}{\eta:\Qp} ((\hapx_\eta u) \to (\hapxb_{\epsilon+\eta} u))
    \land \narrowbreak
    ((\hapxb_\eta u) \to (\hapx_{\epsilon+\eta} u)).
  \end{narrowmultline*}
  We observe that these relations are separated.
  For assuming
  \narrowequation{\fall{\epsilon:\Qp} (\hapname \bsim_\epsilon \hapbname),}
  to show $\hapname = \hapbname$ it suffices to show $(\hapx_\epsilon u) \Leftrightarrow (\hapxb_\epsilon u)$ for all $u:\RC$.
  But $\hapx_\epsilon u$ implies $\hapx_{\epsilon-\theta} u$ for some $\theta$, by roundedness, which together with $\hapname \bsim_\epsilon \hapbname$ implies $\hapxb_\epsilon u$; and the converse is identical.

  Now the first two data the recursion principle requires are the following.
  \begin{itemize}
  \item For any $q:\Q$, we must give an element of $A$, which we denote $(\rcrat(q)\approx_{(\blank)} \blank)$.
  \item For any Cauchy approximation $x$, if we assume defined a function $\Qp \to A$, which we will denote by $\epsilon \mapsto (x_\epsilon \approx_{(\blank)} \blank)$, with the property that
    % \[ \fall{u,v:\RC}{\delta,\epsilon,\eta:\Qp} (x_\delta \approx_\eta u) \to (u\close{\delta+\epsilon} v) \to (x_\epsilon \approx_{\eta+\delta+\epsilon} v) \]
    \begin{equation}
      \fall{u:\RC}{\delta,\epsilon,\eta:\Qp} (x_\delta \approx_\eta u) \to (x_\epsilon \approx_{\eta+\delta+\epsilon} u),\label{eq:appxrec2}
    \end{equation}
    we must give an element of $A$, which we write as $(\rclim(x)\approx_{(\blank)} \blank)$.
  \end{itemize}
  In both cases, we give the required definition by using a nested $(\RC,\closesym)$-recursion, with codomain the subset of $\Qp\to\prop$ consisting of rounded families of mere propositions.
  Thinking of these propositions as zero halves of a binary relation, we will write them as $\epsilon \mapsto (\tap{\epsilon})$, with the symbol $\tapname$ referring to the whole family.
  Now we can write the codomain of these inner recursions precisely as
  \begin{narrowmultline*}
    C \defeq
    \bigg\{ \tapname :\Qp\to\prop \;\;\Big|\;\; \narrowbreak
    \fall{\epsilon:\Qp} \Big((\tap\epsilon) \Leftrightarrow \exis{\theta:\Qp} (\tap{\epsilon-\theta})\Big)\bigg\}
  \end{narrowmultline*}
  We take the required family of relations to be the remnant of the triangle inequality:
  \begin{narrowmultline*}
    (\tapname \bbsim_\epsilon \tapbname) \defeq
    \fall{\eta:\Qp} ((\tap\eta) \to (\tapb{\epsilon+\eta})) \land
    \narrowbreak
    ((\tapb\eta) \to (\tap{\epsilon+\eta})).
  \end{narrowmultline*}
  These relations are separated by the same argument as for $\bsim$, using roundedness of all elements of $C$.

  Note that if such an inner recursion succeeds, it will yield a family of predicates $\hapname : \RC\to\Qp\to \prop$ which are rounded
(since their image in $\Qp\to\prop$ lies in $C$) and satisfy
  \[ \fall{u,v:\RC}{\epsilon:\Qp} (u\close\epsilon v) \to \big((\hapx_{(\blank)} u) \bbsim_\epsilon (\hapx_{(\blank)} u)\big). \]
  Expanding out the definition of $\bbsim$, this yields precisely the third condition for $\hapname$ to belong to $A$; thus it is exactly what we need.

  It is at this point that we can give the definitions~\eqref{eq:RCappx1}--\eqref{eq:RCappx4}, as the first two clauses of each of the two inner recursions, corresponding to rational points and limits.
  In each case, we must verify that the relation is rounded and hence lies in $C$.
  In the rational-rational case~\eqref{eq:RCappx1} this is clear, while in the other cases it follows from an inductive hypothesis.
  (In~\eqref{eq:RCappx2} the relevant inductive hypothesis is that $(\rcrat(q) \approx_{(\blank)} y_\delta) : C$, while in~\eqref{eq:RCappx3} and~\eqref{eq:RCappx4} it is that $(x_\delta \approx_{(\blank)} \blank) : A$.)

  The remaining data of the sub-recursions consist of showing that \eqref{eq:RCappx1}--\eqref{eq:RCappx4} satisfy the triangle inequality on the right with respect to the constructors of $\closesym$.
  There are eight cases --- four in each sub-recursion --- corresponding to the eight possible ways that $u$, $v$, and $w$ in~\eqref{eq:RC-sim-rtri} can be chosen to be rational points or limits.
  First we consider the cases when $u$ is $\rcrat(q)$.
  \begin{enumerate}
  \item Assuming $\rcrat(q)\approx_\phi \rcrat(r)$ and $-\epsilon<|r-s|<\epsilon$, we must show $\rcrat(q)\approx_{\phi+\epsilon} \rcrat(s)$.
    But by definition of $\approx$, this reduces to the triangle inequality for rational numbers.
  \item We assume $\phi,\epsilon,\delta:\Qp$ such that $\rcrat(q)\approx_\phi \rcrat(r)$ and $\rcrat(r) \close{\epsilon-\delta} y_\delta$, and inductively that
    \begin{equation}
      \fall{\psi:\Qp}(\rcrat(q) \approx_{\psi} \rcrat(r)) \to (\rcrat(q) \approx_{\psi+\epsilon-\delta} y_\delta).\label{eq:RCappx-rtri-rrl1}
    \end{equation}
    We assume also that $\psi,\delta\mapsto (\rcrat(q) \approx_{\psi} y_\delta)$ is a Cauchy approximation with respect to $\bbsim$, i.e.\
    \begin{equation}
      \fall{\psi,\xi,\zeta:\Qp} (\rcrat(q) \approx_{\psi} y_\xi) \to (\rcrat(q) \approx_{\psi+\xi+\zeta} y_\zeta),\label{eq:RCappx-rtri-rrl2}
    \end{equation}
    although we do not need this assumption in this case.
    Indeed, \eqref{eq:RCappx-rtri-rrl1} with $\psi\defeq \phi$ yields immediately $\rcrat(q) \approx_{\phi+\epsilon-\delta} y_\delta$, and hence $\rcrat(q) \approx_{\phi+\epsilon} \rclim(y)$ by definition of $\approx$.
  \item We assume $\phi,\epsilon,\delta:\Qp$ such that $\rcrat(q)\approx_\phi \rclim(y)$ and $y_\delta \close{\epsilon-\delta} \rcrat(r)$, and inductively that
    \begin{gather}
      \fall{\psi:\Qp}(\rcrat(q) \approx_{\psi} y_\delta) \to (\rcrat(q) \approx_{\psi+\epsilon-\delta} \rcrat(r)).\label{eq:RCappx-rtri-rlr1}\\
      \fall{\psi,\xi,\zeta:\Qp} (\rcrat(q) \approx_{\psi} y_\xi) \to (\rcrat(q) \approx_{\psi+\xi+\zeta} y_\zeta).\label{eq:RCappx-rtri-rlr2}
    \end{gather}
    By definition, $\rcrat(q)\approx_\phi \rclim(y)$ means that we have $\theta:\Qp$ with $\rcrat(q) \approx_{\phi-\theta} y_\theta$.
    By assumption~\eqref{eq:RCappx-rtri-rlr2}, therefore, we have also $\rcrat(q) \approx_{\phi+\delta} y_\delta$, and then by~\eqref{eq:RCappx-rtri-rlr1} it follows that $\rcrat(q) \approx_{\phi+\epsilon} \rcrat(r)$, as desired.
  \item We assume $\phi,\epsilon,\delta,\eta:\Qp$ such that $\rcrat(q)\approx_\phi \rclim(y)$ and $y_\delta \close{\epsilon-\delta-\eta} z_\eta$, and inductively that
    \begin{gather}
      \fall{\psi:\Qp}(\rcrat(q) \approx_{\psi} y_\delta) \to (\rcrat(q) \approx_{\psi+\epsilon-\delta-\eta} z_\eta), \label{eq:RCappx-rtri-rll1}\\
      \fall{\psi,\xi,\zeta:\Qp} (\rcrat(q) \approx_{\psi} y_\xi) \to (\rcrat(q) \approx_{\psi+\xi+\zeta} y_\zeta), \label{eq:RCappx-rtri-rll2}\\
      \fall{\psi,\xi,\zeta:\Qp} (\rcrat(q) \approx_{\psi} z_\xi) \to (\rcrat(q) \approx_{\psi+\xi+\zeta} z_\zeta). \label{eq:RCappx-rtri-rll3}
    \end{gather}
    Again, $\rcrat(q)\approx_\phi \rclim(y)$ means we have $\xi:\Qp$ with $\rcrat(q) \approx_{\phi-\xi} y_\xi$, while~\eqref{eq:RCappx-rtri-rll2} then implies $\rcrat(q) \approx_{\phi+\delta} y_\delta$ and~\eqref{eq:RCappx-rtri-rll1} implies $\rcrat(q) \approx_{\phi+\epsilon-\eta} z_\eta$.
    But by definition of $\approx$, this implies $\rcrat(q) \approx_{\phi+\epsilon} \rclim(z)$ as desired.
  \end{enumerate}
  Now we move on to the cases when $u$ is $\rclim(x)$, with $x$ a Cauchy approximation.
  In this case, the ambient inductive hypothesis of the definition of $(\rclim(x) \approx_{(\blank)} {\blank}) : A$ is that we have ${(x_\delta \approx_{(\blank)} {\blank})}: A$, so that in addition to being rounded they satisfy the triangle inequality on the right.
  \begin{enumerate}\setcounter{enumi}{4}
  \item Assuming $\rclim(x)\approx_\phi \rcrat(r)$ and $-\epsilon<|r-s|<\epsilon$, we must show $\rclim(x)\approx_{\phi+\epsilon} \rcrat(s)$.
    By definition of $\approx$, the former means $x_\delta \approx_{\phi-\delta} \rcrat(r)$, so that above triangle inequality implies $x_\delta \approx_{\epsilon+\phi-\delta} \rcrat(s)$, hence $\rclim(x)\approx_{\phi+\epsilon} \rcrat(s)$ as desired.
  \item We assume $\phi,\epsilon,\delta:\Qp$ such that $\rclim(x)\approx_\phi \rcrat(r)$ and $\rcrat(r) \close{\epsilon-\delta} y_\delta$, and two unneeded inductive hypotheses.
    %
    By definition, we have $\eta:\Qp$ such that $x_\eta \approx_{\phi-\eta} \rcrat(r)$, so the inductive triangle inequality gives $x_\eta \approx_{\phi+\epsilon-\eta-\delta} y_\delta$.
    The definition of $\approx$ then immediately yields $\rclim(x) \approx_{\phi+\epsilon} \rclim(y)$.
  \item We assume $\phi,\epsilon,\delta:\Qp$ such that $\rclim(x)\approx_\phi \rclim(y)$ and $y_\delta \close{\epsilon-\delta} \rcrat(r)$, and two unneeded inductive hypotheses.
    By definition we have $\xi,\theta:\Qp$ such that $x_\xi \approx_{\phi-\xi-\theta} y_\theta$.
    Since $y$ is a Cauchy approximation, we have $y_\theta \close{\theta+\delta} y_\delta$, so the inductive triangle inequality gives $x_\xi \approx_{\phi+\delta-\xi} y_\delta$ and then $x_\xi \close{\phi+\epsilon-\xi} \rcrat(r)$.
    The definition of $\approx$ then gives $\rclim(x) \approx_{\phi+\epsilon}\rcrat(r)$, as desired.
  \item Finally, we assume $\phi,\epsilon,\delta,\eta:\Qp$ such that $\rclim(x)\approx_\phi \rclim(y)$ and $y_\delta \close{\epsilon-\delta-\eta} z_\eta$.
    Then as before we have $\xi,\theta:\Qp$ with $x_\xi \approx_{\phi-\xi-\theta} y_\theta$, and two applications of the triangle inequality suffices as before.
  \end{enumerate}

  This completes the two inner recursions, and thus the definitions of the families of relations $(\rcrat(q)\approx_{(\blank)}\blank)$ and $(\rclim(x)\approx_{(\blank)}\blank)$.
  Since all are elements of $A$, they are rounded and satisfy the triangle inequality on the right with respect to $\closesym$.
% , and satisfy~\eqref{eq:appxrec2}.
  What remains is to verify the conditions relating to $\bsim$, which is to say that these relations satisfy the triangle inequality on the \emph{left} with respect to the constructors of $\closesym$.
  The four cases correspond to the four choices of rational or limit points for $u$ and $v$ in~\eqref{eq:RC-sim-ltri}, and since they are all mere propositions, we may apply $\RC$-induction and assume that $w$ is also either rational or a limit.
  This yields another eight cases, whose proofs are essentially identical to those just given; so we will not subject the reader to them.
\end{proof}

We can now prove:

\begin{thm}\label{thm:RC-sim-characterization}
  For any $u,v:\RC$ and $\epsilon:\Qp$ we have $(u\close\epsilon v) = (u\approx_\epsilon v)$.
\end{thm}
\begin{proof}
  Since both are mere propositions, it suffices to prove bidirectional implication.
  For the left-to-right direction, we use $\closesym$-induction applied to $C(u,v,\epsilon)\defeq (u\approx_\epsilon v)$.
  Thus, it suffices to consider the four constructors of $\closesym$.
  In each case, $u$ and $v$ are specialized to either rational points or limits, so that the definition of $\approx$ evaluates, and the inductive hypothesis always applies.

  For the right-to-left direction, we use $\RC$-induction to assume that $u$ and $v$ are rational points or limits, allowing $\approx$ to evaluate.
  But now the definitions of $\approx$, and the inductive hypotheses, supply exactly the data required for the relevant constructors of $\closesym$.
\end{proof}

\index{encode-decode method}%
Stretching a point, one might call $\approx$ a fibration of ``codes'' for $\closesym$, with the two directions of the above proof being \encode and \decode respectively.
By the definition of $\approx$, from \cref{thm:RC-sim-characterization} we get equivalences
\begin{align*}
  (\rcrat(q) \close\epsilon \rcrat(r))  &=
  (-\epsilon < q - r < \epsilon)\\
  (\rcrat(q) \close\epsilon \rclim(y)) &=
  \exis{\delta : \Qp} \rcrat(q) \close{\epsilon - \delta} y_\delta\\
  (\rclim(x) \close\epsilon \rcrat(r)) &=
  \exis{\delta : \Qp} x_\delta \close{\epsilon - \delta} \rcrat(r)\\
  (\rclim(x) \close\epsilon \rclim(y)) &=
  \exis{\delta, \eta : \Qp} x_\delta \close{\epsilon - \delta - \eta} y_\eta.
\end{align*}
Our proof also provides the following additional information.

\begin{cor}
  \index{triangle!inequality for R@inequality for $\RC$}%
  \indexsee{inequality!triangle}{triangle inequality}%
  $\closesym$ is rounded\index{rounded!relation} and satisfies the triangle inequality:
    \begin{gather}
      \eqvspaced{
        (u \close\epsilon v)
      }{
        \exis{\theta : \Qp} u \close{\epsilon - \theta} v
      }\\
      (u\close\epsilon v) \to (v\close\delta w) \to (u\close{\epsilon+\delta} w). \label{item:RC-sim-triangle}
    \end{gather}
\end{cor}
% \begin{proof}
%   The construction of $\approx$ showed simultaneously that it is rounded, and satisfies ``triangle inequalities'' such as
%   \[ (u\approx_\epsilon v) \to (v\close\delta w) \to (u\approx_{\epsilon+\delta} w). \]
%   Thus, both properties follow from \cref{thm:RC-sim-characterization}.
% \end{proof}

With the triangle inequality in hand, we can show that ``limits'' of Cauchy approximations actually behave like limits.

\begin{lem}\label{thm:RC-sim-lim}
  For any $u:\RC$, Cauchy approximation $y$, and $\epsilon,\delta:\Qp$, if $u\close\epsilon y_\delta$ then $u\close{\epsilon+\delta} \rclim(y)$.
\end{lem}
\begin{proof}
  We use $\RC$-induction on $u$.
  If $u$ is $\rcrat(q)$, then this is exactly the second constructor of $\closesym$.
  Now suppose $u$ is $\rclim(x)$, and that each $x_\eta$ has the property that for any $y,\epsilon,\delta$, if $x_\eta\close\epsilon y_\delta$ then $x_\eta \close{\epsilon+\delta} \rclim(y)$.
  In particular, taking $y\defeq x$ and $\delta\defeq\eta$ in this assumption, we conclude that $x_\eta \close{\eta+\theta} \rclim(x)$ for any $\eta,\theta:\Qp$.

  Now let $y,\epsilon,\delta$ be arbitrary and assume $\rclim(x) \close\epsilon y_\delta$.
  By roundedness, there is a $\theta$ such that $\rclim(x) \close{\epsilon-\theta} y_\delta$.
  Then by the above observation, for any $\eta$ we have $x_\eta \close{\eta+\theta/2} \rclim(x)$, and hence $x_\eta \close{\epsilon+\eta-\theta/2} y_\delta$ by the triangle inequality.
  Hence, the fourth constructor of $\closesym$ yields $\rclim(x) \close{\epsilon+2\eta+\delta-\theta/2} \rclim(y)$.
  Thus, if we choose $\eta \defeq \theta/4$, the result follows.
\end{proof}

\begin{lem}\label{thm:RC-sim-lim-term}
  For any Cauchy approximation $y$ and any $\delta,\eta:\Qp$ we have $y_\delta \close{\delta+\eta} \rclim(y)$.
\end{lem}
\begin{proof}
  Take $u\defeq y_\delta$ and $\epsilon\defeq \eta$ in the previous lemma.
\end{proof}

\begin{rmk}
  We might have expected to have $y_\delta \close{\delta} \rclim(y)$, but this fails in examples.
  For instance, consider $x$ defined by $x_\epsilon \defeq \epsilon$.
  Its limit is clearly $0$, but we do not have $|\epsilon - 0 |<\epsilon$, only $\le$.
\end{rmk}

As an application, \cref{thm:RC-sim-lim-term} enables us to show that the extensions of Lipschitz functions from \cref{RC-extend-Q-Lipschitz} are unique.

\begin{lem}\label{RC-continuous-eq}
  \index{function!continuous}%
  Let $f,g:\RC\to\RC$ be continuous, in the sense that
  \[ \fall{u:\RC}{\epsilon:\Qp}\exis{\delta:\Qp}\fall{v:\RC} (u\close\delta v) \to (f(u) \close\epsilon f(v)) \]
  and analogously for $g$.
  If $f(\rcrat(q))=g(\rcrat(q))$ for all $q:\Q$, then $f=g$.
\end{lem}
\begin{proof}
  We prove $f(u)=g(u)$ for all $u$ by $\RC$-induction.
  The rational case is just the hypothesis.
  Thus, suppose $f(x_\delta)=g(x_\delta)$ for all $\delta$.
  We will show that $f(\rclim(x))\close\epsilon g(\rclim(x))$ for all $\epsilon$, so that the path constructor of $\RC$ applies.

  Since $f$ and $g$ are continuous, there exist $\theta,\eta$ such that for all $v$, we have
  \begin{align*}
    (\rclim(x)\close\theta v) &\to (f(\rclim(x)) \close{\epsilon/2} f(v))\\
    (\rclim(x)\close\eta v) &\to (g(\rclim(x)) \close{\epsilon/2} g(v)).
  \end{align*}
  Choosing $\delta < \min(\theta,\eta)$, by \cref{thm:RC-sim-lim-term} we have both $\rclim(x)\close\theta y_\delta$ and $\rclim(x)\close\eta y_\delta$.
  Hence
  \[ f(\rclim(x)) \close{\epsilon/2} f(y_\delta) = g(y_\delta) \close{\epsilon/2} g(\rclim(x))\]
  and thus $f(\rclim(x))\close\epsilon g(\rclim(x))$ by the triangle inequality.
\end{proof}

\subsection{The algebraic structure of Cauchy reals}
\label{sec:algebr-struct-cauchy}

We first define the additive structure $(\RC, 0, {+}, {-})$. Clearly, the additive unit element
$0$ is just $\rcrat(0)$, while the additive inverse ${-} : \RC \to \RC$ is obtained as the
extension of the additive inverse ${-} : \Q \to \Q$, using \cref{RC-extend-Q-Lipschitz}
with Lipschitz constant~$1$. We have to work a bit harder for addition.

\begin{lem} \label{RC-binary-nonexpanding-extension}
  Suppose $f : \Q \times \Q \to \Q$ satisfies, for all $q, r, s : \Q$,
  %
  \begin{equation*}
    |f(q, s) - f(r, s)| \leq |q - r|
    \qquad\text{and}\qquad
    |f(q, r) - f(q, s)| \leq |r - s|.
  \end{equation*}
  %
  Then there is a function $\bar{f} : \RC \times \RC \to \RC$ such that
  $\bar{f}(\rcrat(q), \rcrat(r)) = f(q,r)$ for all $q, r : \Q$. Furthermore,
  for all $u, v, w : \RC$ and $q : \Qp$,
  %
  \begin{equation*}
    u \close\epsilon v \Rightarrow \bar{f}(u,w) \close\epsilon \bar{f}(v,w)
    \quad\text{and}\quad
    v \close\epsilon w \Rightarrow \bar{f}(u,v) \close\epsilon \bar{f}(u,w).
  \end{equation*}
\end{lem}

\begin{proof}
  We use $(\RC, {\closesym})$-recursion to construct the curried form of $\bar{f}$ as a map
  $\RC \to A$ where $A$ is the space of non-expanding\index{function!non-expanding}\index{non-expanding function} real-valued
  functions:
  %
  \begin{equation*}
    A \defeq
    \setof{ h : \RC \to \RC |
      \fall{\epsilon : \Qp} \fall{u, v : \RC}
      u \close\epsilon v \Rightarrow h(u) \close\epsilon h(v)
    }.
  \end{equation*}
  %
  We shall also need a suitable $\bsim_\epsilon$ on $A$, which we define as
  %
  \begin{equation*}
    (h \bsim_\epsilon k) \defeq \fall{u : \RC} h(u) \close\epsilon k(u).
  \end{equation*}
  %
  Clearly, if $\fall{\epsilon : \Qp} h \bsim_\epsilon k$ then $h(u) = k(u)$ for all $u :
  \RC$, so $\bsim$ is separated.

  For the base case we define $\bar{f}(\rcrat(q)) : A$, where $q : \Q$, as the
  extension of the Lipschitz map $\lam{r} f(q,r)$ from $\Q \to \Q$ to $\RC \to \RC$, as
  constructed in \cref{RC-extend-Q-Lipschitz} with Lipschitz constant~$1$. Next, for a
  Cauchy approximation $x$, we define $\bar{f}(\rclim(x)) : \RC \to \RC$ as
  %
  \begin{equation*}
    \bar{f}(\rclim(x))(v) \defeq \rclim (\lam{\epsilon} \bar{f}(x_\epsilon)(v)).
  \end{equation*}
  %
  For this to be a valid definition, $\lam{\epsilon} \bar{f}(x_\epsilon)(v)$ should be a
  Cauchy approximation, so consider any $\delta, \epsilon : \Q$. Then by assumption
  $\bar{f}(x_\delta) \bsim_{\delta + \epsilon} \bar{f}(x_\epsilon)$, hence
  $\bar{f}(x_\delta)(v) \close{\delta + \epsilon} \bar{f}(x_\epsilon)(v)$. Furthermore,
  $\bar{f}(\rclim(x))$ is non-expanding because $\bar{f}(x_\epsilon)$ is such by induction
  hypothesis. Indeed, if $u \close\epsilon v$ then, for all $\epsilon : \Q$,
  %
  \begin{equation*}
    \bar{f}(x_{\epsilon/3})(u) \close{\epsilon/3} \bar{f}(x_{\epsilon/3})(v),
  \end{equation*}
  %
  therefore $\bar{f}(\rclim(x))(u) \close\epsilon \bar{f}(\rclim(x))(v)$ by the fourth constructor of $\closesym$.

  We still have to check four more conditions, let us illustrate just one. Suppose
  $\epsilon : \Qp$ and for some $\delta : \Qp$ we have $\rcrat(q) \close{\epsilon - \delta}
  y_\delta$ and $\bar{f}(\rcrat(q)) \bsim_{\epsilon - \delta} \bar{f}(y_\delta)$. To show
  $\bar{f}(\rcrat(q)) \bsim_\epsilon \bar{f}(\rclim(y))$, consider any $v : \RC$ and observe that
  %
  \begin{equation*}
    \bar{f}(\rcrat(q))(v) \close{\epsilon - \delta} \bar{f}(y_\delta)(v).
  \end{equation*}
  %
  Therefore, by the second constructor of $\closesym$, we have
  \narrowequation{\bar{f}(\rcrat(q))(v) \close\epsilon \bar{f}(\rclim(y))(v)}
  as required.
\end{proof}

We may apply \cref{RC-binary-nonexpanding-extension} to any bivariate rational function
which is non-expanding separately in each variable. Addition is such a function, therefore
we get ${+} : \RC \times \RC \to \RC$.
\indexdef{addition!of Cauchy reals}%
Furthermore, the extension is unique as long as we
require it to be non-expanding in each variable, and just as in the univariate case,
identities on rationals extend to identities on reals. Since composition of non-expanding
maps is again non-expanding, we may conclude that addition satisfies the usual properties,
such as commutativity and associativity.
\index{associativity!of addition!of Cauchy reals}%
Therefore, $(\RC, 0, {+}, {-})$ is a commutative
group.

We may also apply \cref{RC-binary-nonexpanding-extension} to the functions $\min : \Q \times
\Q \to \Q$ and $\max : \Q \times \Q \to \Q$, which turns $\RC$ into a lattice. The partial
order $\leq$ on $\RC$ is defined in terms of $\max$ as
%
\symlabel{leq-RC}
\index{order!non-strict}%
\index{non-strict order}%
\begin{equation*}
  (u \leq v) \defeq (\max(u, v) = v).
\end{equation*}
%
The relation $\leq$ is a partial order because it is such on $\Q$, and the axioms of a
partial order are expressible as equations in terms of $\min$ and $\max$, so they transfer
to $\RC$.

\index{absolute value}%
Another function which extends to $\RC$ by the same method is the absolute value $|{\blank}|$.
Again, it has the expected properties because they transfer from $\Q$ to $\RC$.

\symlabel{lt-RC}
From $\leq$ we get the strict order $<$ by
\index{strict!order}%
\index{order!strict}%
%
\begin{equation*}
  (u < v) \defeq \exis{q, r : \Q} (u \leq \rcrat(q)) \land (q < r) \land (\rcrat(r) \leq v).
\end{equation*}
%
That is, $u < v$ holds when there merely exists a pair of rational numbers $q < r$ such that $x \leq
\rcrat(q)$ and $\rcrat(r) \leq v$. It is not hard to check that $<$ is irreflexive and
transitive, and has other properties that are expected for an ordered field.
The archimedean principle follows directly from the definition of~$<$.

\index{ordered field!archimedean}%
\begin{thm}[Archimedean principle for $\RC$] \label{RC-archimedean}
  %
  For every $u, v : \RC$ such that $u < v$ there merely exists $q : \Q$ such that $u < q < v$.
\end{thm}

\begin{proof}
  From $u < v$ we merely get $r, s : \Q$ such that $u \leq r < s \leq v$, and we may take $q
  \defeq (r + s) / 2$.
\end{proof}

We now have enough structure on $\RC$ to express $u \close\epsilon v$ with standard concepts.

\begin{lem}\label{thm:RC-le-grow}
  If $q:\Q$ and $u:\RC$ satisfy $u\le \rcrat(q)$, then for any $v:\RC$ and $\epsilon:\Qp$, if $u\close\epsilon v$ then $v\le \rcrat(q+\epsilon)$.
\end{lem}
\begin{proof}
  Note that the function $\max(\rcrat(q),\blank):\RC\to\RC$ is Lipschitz with constant $1$.
  First consider the case when $u=\rcrat(r)$ is rational.
  For this we use induction on $v$.
  If $v$ is rational, then the statement is obvious.
  If $v$ is $\rclim(y)$, we assume inductively that for any $\epsilon,\delta$, if $\rcrat(r)\close\epsilon y_\delta$ then $y_\delta \le \rcrat(q+\epsilon)$, i.e.\ $\max(\rcrat(q+\epsilon),y_\delta)=\rcrat(q+\epsilon)$.

  Now assuming $\epsilon$ and $\rcrat(r)\close\epsilon \rclim(y)$, we have $\theta$ such that $\rcrat(r)\close{\epsilon-\theta} \rclim(y)$, hence $\rcrat(r)\close\epsilon y_\delta$ whenever $\delta<\theta$.
  Thus, the inductive hypothesis gives $\max(\rcrat(q+\epsilon),y_\delta)=\rcrat(q+\epsilon)$ for such $\delta$.
  But by definition,
  \[\max(\rcrat(q+\epsilon),\rclim(y)) \jdeq \rclim(\lam{\delta} \max(\rcrat(q+\epsilon),y_\delta)).\]
  Since the limit of an eventually constant Cauchy approximation is that constant, we have
  \[\max(\rcrat(q+\epsilon),\rclim(y)) = \rcrat(q+\epsilon),\] hence $\rclim(y)\le \rcrat(q+\epsilon)$.

  Now consider a general $u:\RC$.
  Since $u\le \rcrat(q)$ means $\max(\rcrat(q),u)=\rcrat(q)$, the assumption $u\close\epsilon v$ and the Lipschitz property of $\max(\rcrat(q),-)$ imply $\max(\rcrat(q),v) \close\epsilon \rcrat(q)$.
  Thus, since $\rcrat(q)\le \rcrat(q)$, the first case implies $\max(\rcrat(q),v) \le \rcrat(q+\epsilon)$, and hence $v\le \rcrat(q+\epsilon)$ by transitivity of $\le$.
\end{proof}

\begin{lem}\label{thm:RC-lt-open}
  Suppose $q:\Q$ and $u:\RC$ satisfy $u<\rcrat(q)$.  Then:
  \begin{enumerate}
  \item For any $v:\RC$ and $\epsilon:\Qp$, if $u\close\epsilon v$ then $v< \rcrat(q+\epsilon)$.\label{item:RCltopen1}
  \item There exists $\epsilon:\Qp$ such that for any $v:\RC$, if $u\close\epsilon v$ we have $v<\rcrat(q)$.\label{item:RCltopen2}
  \end{enumerate}
\end{lem}
\begin{proof}
  By definition, $u<\rcrat(q)$ means there is $r:\Q$ with $r<q$ and $u\le \rcrat(r)$.
  Then by \cref{thm:RC-le-grow}, for any $\epsilon$, if $u\close\epsilon v$ then $v\le \rcrat(r+\epsilon)$.
  Conclusion~\ref{item:RCltopen1} follows immediately since $r+\epsilon<q+\epsilon$, while for~\ref{item:RCltopen2} we can take any $\epsilon <q-r$.
\end{proof}

We are now able to show that the auxiliary relation $\closesym$ is what we think it is.

\begin{thm} \label{RC-sim-eqv-le}
  \index{distance}%
  $\eqv{(u \close\epsilon v)}{(|u - v| < \rcrat(\epsilon))}$
  for all $u, v : \RC$ and $\epsilon : \Qp$.
\end{thm}
\begin{proof}
  The Lipschitz properties of subtraction and absolute value imply that if $u\close\epsilon v$, then $|u-v| \close\epsilon |u-u| = 0$.
  Thus, for the left-to-right direction, it will suffice to show that if $u\close\epsilon 0$, then $|u|<\rcrat(\epsilon)$.
  We proceed by $\RC$-induction on $u$.

  If $u$ is rational, the statement follows immediately since absolute value and order extend the standard ones on $\Qp$.
  If $u$ is $\rclim(x)$, then by roundedness we have $\theta:\Qp$ with $\rclim(x)\close{\epsilon-\theta} 0$.
  By the triangle inequality, therefore, we have $x_{\theta/3} \close{\epsilon-2\theta/3} 0$, so the inductive hypothesis yields $|x_{\theta/3}|<\rcrat(\epsilon-2\theta/3)$.
  But $x_{\theta/3} \close{2\theta/3} \rclim(x)$, hence $|x_{\theta/3}| \close{2\theta/3} |\rclim(x)|$ by the Lipschitz property, so \cref{thm:RC-lt-open}\ref{item:RCltopen1} implies $|\rclim(x)|<\rcrat(\epsilon)$.

  In the other direction, we use $\RC$-induction on $u$ and $v$.
  If both are rational, this is the first constructor of $\closesym$.

  If $u$ is $\rcrat(q)$ and $v$ is $\rclim(y)$, we assume inductively that for any $\epsilon,\delta$, if $|\rcrat(q)-y_\delta|<\rcrat(\epsilon)$ then $\rcrat(q) \close{\epsilon} y_\delta$.
  Fix an $\epsilon$ such that $|\rcrat(q) - \rclim(y)|<\rcrat(\epsilon)$.
  Since $\Q$ is order-dense in $\RC$, there exists $\theta<\epsilon$ with $|\rcrat(q) - \rclim(y)|<\rcrat(\theta)$.
  Now for any $\delta,\eta$ we have $\rclim(y)\close{2\delta} y_\delta$, hence by the Lipschitz property
  \[ |\rcrat(q) - \rclim(y)| \close{\delta+\eta} |\rcrat(q) - y_\delta|. \]
  Thus, by \cref{thm:RC-lt-open}\ref{item:RCltopen1}, we have $|\rcrat(q) - y_\delta| < \rcrat(\theta+2\delta)$.
  So by the inductive hypothesis, $\rcrat(q) \close{\theta+2\delta} y_\delta$, and thus $\rcrat(q)\close{\theta+4\delta} \rclim(y)$ by the triangle inequality.
  Thus, it suffices to choose $\delta \defeq (\epsilon-\theta)/4$.

  The remaining two cases are entirely analogous.
\end{proof}

\indexdef{multiplication!of Cauchy reals}%
Next, we would like to equip $\RC$ with multiplicative structure. For each $q : \Q$ the
map $r \mapsto q \cdot r$ is Lipschitz with constant\footnote{We defined Lipschitz
  constants as \emph{positive} rational numbers.} $|q| + 1$, and so we can extend it to
multiplication by $q$ on the real numbers. Therefore $\RC$ is a vector space\index{vector!space} over $\Q$.
In general, we can define multiplication of real numbers as
%
\begin{equation}
  u \cdot v \defeq
  {\textstyle \frac{1}{2}} \cdot ((u + v)^2 - u^2 - v^2),\label{mult-from-square}
\end{equation}
%
so we just need squaring\index{squaring function} $u \mapsto u^2$ as a map $\RC \to \RC$. Squaring is not a
Lipschitz map, but it is Lipschitz on every bounded domain, which allows us to patch it
together. Define the open and closed intervals
%
\indexdef{interval!open and closed}%
\indexdef{open!interval}%
\indexdef{closed!interval}%
\begin{equation*}
  [u,v] \defeq \setof{ x : \RC | u \leq x \leq v }
  \qquad\text{and}\qquad
  (u,v) \defeq \setof{ x : \RC | u < x < v }.
\end{equation*}
%
Although technically an element of $[u,v]$ or $(u,v)$ is a Cauchy real number together with a proof, since the latter inhabits a mere proposition it is uninteresting.
Thus, as is common with subset types, we generally write simply $x:[u,v]$ whenever $x:\RC$ is such that $u\leq x \leq v$, and similarly.

\begin{thm} \label{RC-squaring}
  %
  There exists a unique function ${(\blank)}^2 : \RC \to \RC$ which extends squaring $q \mapsto
  q^2$ of rational numbers and satisfies
  %
  \begin{equation*}
    \fall{n : \N}
    \fall{u, v : [-n, n]}
    |u^2 - v^2| \leq 2 \cdot n \cdot |u - v|.
  \end{equation*}
\end{thm}

\begin{proof}
  We first observe that for every $u : \RC$ there merely exists $n : \N$ such that $-n
  \leq u \leq n$, see \cref{ex:traditional-archimedean}, so the map
  %
  \begin{equation*}
    e : \Parens{\sm{n : \N} [-n, n]} \to \RC
    \qquad\text{defined by}\qquad
    e(n, x) \defeq x
  \end{equation*}
  %
  is surjective. Next, for each $n : \N$, the squaring map
  %
  \begin{equation*}
    s_n : \setof{ q : \Q | -n \leq q \leq n } \to \Q
    \qquad\text{defined by}\qquad
    s_n(q) \defeq q^2
  \end{equation*}
  %
  is Lipschitz with constant $2 n$, so we can use \cref{RC-extend-Q-Lipschitz} to
  extend it to a map $\bar{s}_n : [-n, n] \to \RC$ with Lipschitz constant $2 n$, see
  \cref{RC-Lipschitz-on-interval} for details. The maps $\bar{s}_n$ are compatible: if
  $m < n$ for some $m, n : \N$ then $s_n$ restricted to $[-m, m]$ must agree with $s_m$
  because both are Lipschitz, and therefore continuous in the sense
  of~\cref{RC-continuous-eq}. Therefore, by \cref{lem:images_are_coequalizers} the map
  %
  \begin{equation*}
    \Parens{\sm{n : \N} [-n, n]} \to \RC,
    \qquad\text{given by}\qquad
    (n, x) \mapsto s_n(x)
  \end{equation*}
  %
  factors uniquely through $\RC$ to give us the desired function.
\end{proof}

At this point we have the ring structure of the reals and the archimedean order. To
establish $\RC$ as an archimedean ordered field, we still need inverses.

\begin{thm}
  \index{apartness}%
  A Cauchy real is invertible if, and only if, it is apart from zero.
\end{thm}

\begin{proof}
  First, suppose $u : \RC$ has an inverse $v : \RC$ By the archimedean principle there is $q :
  \Q$ such that $|v| < q$. Then $1 = |u v| < |u| \cdot v < |u| \cdot q$ and hence $|u| >
  1/q$, which is to say that $u \apart 0$.

  For the converse we construct the inverse map
  %
  \begin{equation*}
    ({\blank})^{-1} : \setof{ u : \RC | u \apart 0 } \to \RC
  \end{equation*}
  %
  by patching together functions, similarly to the construction of squaring in
  \cref{RC-squaring}. We only outline the main steps. For every $q : \Q$ let
  %
  \begin{equation*}
    [q, \infty) \defeq \setof{u : \RC | q \leq u}
    \qquad\text{and}\qquad
    (-\infty, q] \defeq \setof{u : \RC | u \leq -q}.
  \end{equation*}
  %
  Then, as $q$ ranges over $\Qp$, the types $(-\infty, q]$ and $[q, \infty)$ jointly cover
  $\setof{u : \RC | u \apart 0}$. On each such $[q, \infty)$ and $(-\infty, q]$ the
  inverse function is obtained by an application of \cref{RC-extend-Q-Lipschitz}
  with Lipschitz constant $1/q^2$. Finally, \cref{lem:images_are_coequalizers}
  guarantees that the inverse function factors uniquely through $\setof{ u : \RC | u
    \apart 0 }$.
\end{proof}

We summarize the algebraic structure of $\RC$ with a theorem.

\begin{thm} \label{RC-archimedean-ordered-field}
  The Cauchy reals form an archimedean ordered field.
\end{thm}

\subsection{Cauchy reals are Cauchy complete}
\label{sec:cauchy-reals-cauchy-complete}

We constructed $\RC$ by closing $\Q$ under limits of Cauchy approximations, so it better
be the case that $\RC$ is Cauchy complete. Thanks to \cref{RC-sim-eqv-le} there is no
difference between a Cauchy approximation $x : \Qp \to \RC$ as defined in the construction
of $\RC$, and a Cauchy approximation in the sense of \cref{defn:cauchy-approximation}
(adapted to $\RC$).

Thus, given a Cauchy approximation $x : \Qp \to \RC$ it is quite natural to expect that
$\rclim(x)$ is its limit, where the notion of limit is defined as in
\cref{defn:cauchy-approximation}. But this is so by \cref{RC-sim-eqv-le} and
\cref{thm:RC-sim-lim-term}. We have proved:

\begin{thm}
  Every Cauchy approximation in $\RC$ has a limit.
\end{thm}

An archimedean ordered field in which every Cauchy approximation has a limit is called
\define{Cauchy complete}.
\indexdef{Cauchy!completeness}%
\indexdef{complete!ordered field, Cauchy}%
\index{ordered field}%
The Cauchy reals are the least such field.

\begin{thm} \label{RC-initial-Cauchy-complete}
  The Cauchy reals embed into every Cauchy complete ar\-chi\-me\-de\-an ordered field.
\end{thm}

\begin{proof}
  \index{limit!of a Cauchy approximation}%
  Suppose $F$ is a Cauchy complete archimedean ordered field. Because limits are unique,
  there is an operator $\lim$ which takes Cauchy approximations in $F$ to their limits. We
  define the embedding $e : \RC \to F$ by $(\RC, {\closesym})$-recursion as
  %
  \begin{equation*}
    e(\rcrat(q)) \defeq q
    \qquad\text{and}\qquad
    e(\rclim(x)) \defeq \lim (e \circ x).
  \end{equation*}
  %
  A suitable $\bsim$ on $F$ is
  %
  \begin{equation*}
    (a \bsim_\epsilon b) \defeq |a - b| < \epsilon.
  \end{equation*}
  %
  This is a separated relation because $F$ is archimedean. The rest of the clauses for
  $(\RC, {\closesym})$-recursion are easily checked. One would also have to check that $e$ is
  an embedding of ordered fields which fixes the rationals.
\end{proof}

\index{real numbers!Cauchy|)}%

\section{Comparison of Cauchy and Dedekind reals}
\label{sec:comp-cauchy-dedek}

\index{real numbers!Dedekind|(}%
\index{real numbers!Cauchy|(}%
\index{depression|(}

Let us also say something about the relationship between the Cauchy and Dedekind reals. By
\cref{RC-archimedean-ordered-field}, $\RC$ is an archimedean ordered field. It is also
admissible\index{ordered field!admissible} for $\Omega$, as can be easily checked. (In case $\Omega$ is the initial
$\sigma$-frame
\index{initial!sigma-frame@$\sigma$-frame}%
\index{sigma-frame@$\sigma$-frame!initial}%
it takes a simple induction, while in other cases it is immediate.)
Therefore, by \cref{RD-final-field} there is an embedding of ordered fields
%
\begin{equation*}
  \RC \to \RD
\end{equation*}
%
which fixes the rational numbers.
(We could also obtain this from \cref{RC-initial-Cauchy-complete,RD-cauchy-complete}.)
In general we do not expect $\RC$ and $\RD$ to coincide
without further assumptions.

\begin{lem} \label{lem:untruncated-linearity-reals-coincide}
  %
  If for every $x : \RD$ there merely exists
  %
  \begin{equation}
    \label{eq:untruncated-linearity}
    c : \prd{q, r : \Q} (q < r) \to (q < x) + (x < r)
  \end{equation}
  %
  then the Cauchy and Dedekind reals coincide.
\end{lem}

\begin{proof}
  Note that the type in~\eqref{eq:untruncated-linearity} is an untruncated variant
  of~\eqref{eq:RD-linear-order}, which states that~$<$ is a weak linear order.
  We already know that $\RC$ embeds into $\RD$, so it suffices to show that every Dedekind
  real merely is the limit of a Cauchy sequence\index{Cauchy!sequence} of rational numbers.

  Consider any $x : \RD$. By assumption there merely exists $c$ as in the statement of the
  lemma, and by inhabitation of cuts\index{cut!Dedekind} there merely exist $a, b : \Q$ such that $a < x < b$.
  We construct a sequence\index{sequence} $f : \N \to \setof{ \pairr{q, r} \in \Q \times \Q | q < r }$ by
  recursion:
  %
  \begin{enumerate}
  \item Set $f(0) \defeq \pairr{a, b}$.
  \item Suppose $f(n)$ is already defined as $\pairr{q_n, r_n}$ such that $q_n < r_n$.
    Define $s \defeq (2 q_n + r_n)/3$ and $t \defeq (q_n + 2 r_n)/3$. Then $c(s,t)$
    decides between $s < x$ and $x < t$. If it decides $s < x$ then we set $f(n+1) \defeq
    \pairr{s, r_n}$, otherwise $f(n+1) \defeq \pairr{q_n, t}$.
  \end{enumerate}
  %
  Let us write $\pairr{q_n, r_n}$ for the $n$-th term of the sequence~$f$. Then it is easy
  to see that $q_n < x < r_n$ and $|q_n - r_n| \leq (2/3)^n \cdot |q_0 - r_0|$ for all $n
  : \N$. Therefore $q_0, q_1, \ldots$ and $r_0, r_1, \ldots$ are both Cauchy sequences
  converging to the Dedekind cut~$x$. We have shown that for every $x : \RD$ there merely
  exists a Cauchy sequence converging to $x$.
\end{proof}

The lemma implies that either countable choice or excluded middle suffice for coincidence
of $\RC$ and $\RD$.

\begin{cor} \label{when-reals-coincide}
  \index{axiom!of choice!countable}%
  \index{excluded middle}%
  If excluded middle or countable choice holds then $\RC$ and $\RD$ are equivalent.
\end{cor}

\begin{proof}
  If excluded middle holds then $(x < y) \to (x < z) + (z < y)$ can be proved: either $x <
  z$ or $\lnot (x < z)$. In the former case we are done, while in the latter we get $z <
  y$ because $z \leq x < y$. Therefore, we get~\eqref{eq:untruncated-linearity} so that we
  can apply \cref{lem:untruncated-linearity-reals-coincide}.

  Suppose countable choice holds. The set $S = \setof{ \pairr{q, r} \in \Q \times \Q | q <
    r }$ is equivalent to $\N$, so we may apply countable choice to the statement that $x$
  is located,
  %
  \begin{equation*}
    \fall{\pairr{q, r} : S} (q < x) \lor (x < r).
  \end{equation*}
  %
  Note that $(q < x) \lor (x < r)$ is expressible as an existential statement $\exis{b :
    \bool} (b = \bfalse \to q < x) \land (b = \btrue \to x < r)$. The (curried form) of
  the choice function is then precisely~\eqref{eq:untruncated-linearity} so that
  \cref{lem:untruncated-linearity-reals-coincide} is applicable again.
\end{proof}

\index{real numbers!Dedekind|)}%
\index{real numbers!Cauchy|)}%
\index{real numbers!agree}%

\index{depression|)}

\section{Compactness of the interval}
\label{sec:compactness-interval}

\index{mathematics!classical|(}%
\index{mathematics!constructive|(}%

We already pointed out that our constructions of reals are entirely compatible with
classical logic. Thus, by assuming the law of excluded middle~\eqref{eq:lem} and the axiom
of choice~\eqref{eq:ac} we could develop classical analysis,\index{classical!analysis}\index{analysis!classical} which would essentially
amount to copying any standard book on analysis.

\index{analysis!constructive}%
\index{constructive!analysis}%
Nevertheless, anyone interested in computation, for example a numerical analyst, ought to
be curious about developing analysis in a computationally meaningful setting. That
analysis in a constructive setting is even possible was demonstrated by~\cite{Bishop1967}.
As a sample of the differences and similarities between classical and constructive
analysis we shall briefly discuss just one topic---compactness of the closed interval
$[0,1]$ and a couple of theorems surrounding the concept.

Compactness is no exception to the common phenomenon in constructive mathematics that
classically equivalent notions bifurcate. The three most frequently used notions of
compactness are:
%
\indexdef{compactness}%
\begin{enumerate}
\item \define{metrically compact:} ``Cauchy complete and totally bounded'',
  \indexdef{metrically compact}%
  \indexdef{compactness!metric}%
\item \define{Bolzano--Weierstra\ss{} compact:} ``every sequence has a convergent subsequence'',
  \index{compactness!Bolzano--Weierstrass@Bolzano--Weierstra\ss{}}%
  \indexsee{Bolzano--Weierstrass@Bolzano--Weierstra\ss{}}{compactness}%
  \index{sequence}%
\item \define{Heine--Borel compact:} ``every open cover has a finite subcover''.
  \index{compactness!Heine--Borel}%
  \indexsee{Heine--Borel}{compactness}%
\end{enumerate}
%
These are all equivalent in classical mathematics.
Let us see how they fare in homotopy type theory. We can use either the Dedekind or the
Cauchy reals, so we shall denote the reals just as~$\R$. We first recall several basic
definitions.

\indexsee{space!metric}{metric space}
\index{metric space|(}%

\begin{defn} \label{defn:metric-space}
  A \define{metric space}
  \indexdef{metric space}%
  $(M, d)$ is a set $M$ with a map $d : M \times M \to \R$
  satisfying, for all $x, y, z : M$,
  %
  \begin{align*}
    d(x,y) &\geq 0, &
    d(x,y) &= d(y,x), \\
    d(x,y) &= 0 \Leftrightarrow x = y, &
    d(x,z) &\leq d(x,y) + d(y,z).
  \end{align*}
  %
\end{defn}

\begin{defn} \label{defn:complete-metric-space}
  A \define{Cauchy approximation}
  \index{Cauchy!approximation}%
  in $M$ is a sequence $x : \Qp \to M$ satisfying
  %
  \begin{equation*}
    \fall{\delta, \epsilon} d(x_\delta, x_\epsilon) < \delta + \epsilon.
  \end{equation*}
  %
  \index{limit!of a Cauchy approximation}%
  The \define{limit} of a Cauchy approximation $x : \Qp \to M$ is a point $\ell : M$
  satisfying
  %
  \begin{equation*}
    \fall{\epsilon, \theta : \Qp} d(x_\epsilon, \ell) < \epsilon + \theta.
  \end{equation*}
  %
  \indexdef{metric space!complete}%
  \indexdef{complete!metric space}%
  A \define{complete metric space} is one in which every Cauchy approximation has a limit.
\end{defn}

\begin{defn} \label{defn:total-bounded-metric-space}
  For a positive rational $\epsilon$, an \define{$\epsilon$-net}
  \indexdef{epsilon-net@$\epsilon$-net}%
  in a metric space $(M,
  d)$ is an element of
  %
  \begin{equation*}
    \sm{n : \N}{x_1, \ldots, x_n : M}
    \fall{y : M} \exis{k \leq n} d(x_k, y) < \epsilon.
  \end{equation*}
  %
  In words, this is a finite sequence of points $x_1, \ldots, x_n$ such that every point
  in $M$ merely is within $\epsilon$ of some~$x_k$.

  A metric space $(M, d)$ is \define{totally bounded}
  \indexdef{totally bounded metric space}%
  \indexdef{metric space!totally bounded}%
  when it has $\epsilon$-nets of all
  sizes:
  %
  \begin{equation*}
    \prd{\epsilon : \Qp}
    \sm{n : \N}{x_1, \ldots, x_n : M}
    \fall{y : M} \exis{k \leq n} d(x_k, y) < \epsilon.
  \end{equation*}
\end{defn}

\begin{rmk}
  In the definition of total boundedness we used sloppy notation $\sm{n : \N}{x_1, \ldots, x_n : M}$. Formally, we should have written $\sm{x : \lst{M}}$ instead,
  where $\lst{M}$ is the inductive type of finite lists\index{type!of lists} from \cref{sec:bool-nat}.
  However, that would make the rest of the statement a bit more cumbersome to express.
\end{rmk}

Note that in the definition of total boundedness we require pure existence of an
$\epsilon$-net, not mere existence. This way we obtain a function which assigns to each
$\epsilon : \Qp$ a specific $\epsilon$-net. Such a function might be called a ``modulus of
total boundedness''. In general, when porting classical metric notions to homotopy type
theory, we should use propositional truncation sparingly, typically so that we avoid
asking for a non-constant map from $\R$ to $\Q$ or $\N$. For instance, here is the
``correct'' definition of uniform continuity.

\begin{defn} \label{defn:uniformly-continuous}
  A map $f : M \to \R$ on a metric space is \define{uniformly continuous}
  \indexdef{function!uniformly continuous}%
  \indexdef{uniformly continuous function}%
  when
  %
  \begin{equation*}
    \prd{\epsilon : \Qp}
    \sm{\delta : \Qp}
    \fall{x, y : M}
    d(x,y) < \delta \Rightarrow |f(x) - f(y)| < \epsilon.
  \end{equation*}
  %
  In particular, a uniformly continuous map has a modulus of uniform continuity\indexdef{modulus!of uniform continuity},
  which is a function that assigns to each $\epsilon$ a corresponding $\delta$.
\end{defn}

Let us show that $[0,1]$ is compact in the first sense.

\begin{thm} \label{analysis-interval-ctb}
  \index{compactness!metric}%
  \index{interval!open and closed}%
  The closed interval $[0,1]$ is complete and totally bounded.
\end{thm}

\begin{proof}
  Given $\epsilon : \Qp$, there is $n : \N$ such that $2/k < \epsilon$, so we may take the
  $\epsilon$-net $x_i = i/k$ for $i = 0, \ldots, k-1$. This is an $\epsilon$-net because,
  for every $y : [0,1]$ there merely exists $i$ such that $0 \leq i < k$ and $(i -
  1)/k < y < (i+1)/k$, and so $|y - x_i| < 2/k < \epsilon$.

  For completeness of $[0,1]$, consider a Cauchy approximation $x : \Qp \to
  [0,1]$ and let $\ell$ be its limit in $\R$. Since $\max$ and $\min$ are Lipschitz maps,
  the retraction $r : \R \to [0,1]$ defined by $r(x) \defeq \max(0, \min(1, x))$ commutes
  with limits of Cauchy approximations, therefore
  %
  \begin{equation*}
    r(\ell) =
    r (\lim x) =
    \lim (r \circ x) =
    r (\lim x) =
    \ell,
  \end{equation*}
  %
  which means that $0 \leq \ell \leq 1$, as required.
\end{proof}

We thus have at least one good notion of compactness in homotopy type theory.
Unfortunately, it is limited to metric spaces because total boundedness is a metric
notion. We shall consider the other two notions shortly, but first we prove that a
uniformly continuous map on a totally bounded space has a \define{supremum},
\indexsee{least upper bound}{supremum}%
i.e.\ an upper bound which is less than or equal to all other upper bounds.

\begin{thm} \label{ctb-uniformly-continuous-sup}
  %
  \indexdef{supremum!of uniformly continuous function}%
  A uniformly continuous map $f : M \to \R$ on a totally bounded metric space
  $(M, d)$ has a supremum $m : \R$. For every $\epsilon : \Qp$ there exists $u : M$ such
  that $|m - f(u)| < \epsilon$.
\end{thm}

\begin{proof}
  Let $h : \Qp \to \Qp$ be the modulus of uniform continuity of~$f$.
  We define an approximation $x : \Qp \to \R$ as follows: for any $\epsilon : \Q$ total
  boundedness of $M$ gives a $h(\epsilon)$-net $y_0, \ldots, y_n$. Define
  %
  \begin{equation*}
    x_\epsilon \defeq \max (f(y_0), \ldots, f(y_n)).
  \end{equation*}
  %
  We claim that $x$ is a Cauchy approximation. Consider any $\epsilon, \eta : \Q$, so that
  %
  \begin{equation*}
    x_\epsilon \jdeq \max (f(y_0), \ldots, f(y_n))
    \quad\text{and}\quad
    x_\eta \jdeq \max (f(z_0), \ldots, f(z_m))
  \end{equation*}
  %
  for some $h(\epsilon)$-net $y_0, \ldots, y_n$ and $h(\eta)$-net $z_0, \ldots, z_m$.
  Every $z_i$ is merely $h(\epsilon)$-close to some $y_j$, therefore $|f(z_i) - f(y_j)| <
  \epsilon$, from which we may conclude that
  %
  \begin{equation*}
    f(z_i) < \epsilon + f(y_j) \leq \epsilon + x_\epsilon,
  \end{equation*}
  %
  therefore $x_\eta < \epsilon + x_\epsilon$. Symmetrically we obtain $x_\eta < \eta +
  x_\eta$, therefore $|x_\eta - x_\epsilon| < \eta + \epsilon$.

  We claim that $m \defeq \lim x$ is the supremum of~$f$. To prove that $f(x) \leq m$ for
  all $x : M$ it suffices to show $\lnot (m < f(x))$. So suppose to the contrary that $m <
  f(x)$. There is $\epsilon : \Qp$ such that $m + \epsilon < f(x)$. But now merely for
  some $y_i$ participating in the definition of $x_\epsilon$ we get $|f(x) - f(y_i) <
  \epsilon$, therefore $m < f(x) - \epsilon < f(y_i) \leq m$, a contradiction.

  We finish the proof by showing that $m$ satisfies the second part of the theorem, because
  it is then automatically a least upper bound. Given any $\epsilon : \Qp$, on one hand
  $|m - f(x_{\epsilon/2})| < 3 \epsilon/4$, and on the other $|f(x_{\epsilon/2}) - f(y_i)| <
  \epsilon/4$ merely for some $y_i$ participating in the definition of $x_{\epsilon/2}$,
  therefore by taking $u \defeq y_i$ we obtain $|m - f(u)| < \epsilon$ by triangle
  inequality.
\end{proof}

Now, if in \cref{ctb-uniformly-continuous-sup} we also knew that $M$ were complete, we
could hope to weaken the assumption of uniform continuity to continuity, and strengthen
the conclusion to existence of a point at which the supremum is attained. The usual proofs
of these improvements rely on the facts that in a complete totally bounded space
%
\begin{enumerate}
\item continuity implies uniform continuity, and
\item every sequence has a convergent subsequence.
\end{enumerate}
%
The first statement follows easily from Heine--Borel compactness, and the second is just
Bolzano--Weierstra\ss{} compactness.
\index{compactness!Bolzano--Weierstrass@Bolzano--Weierstra\ss{}}%
Unfortunately, these are both somewhat problematic. Let
us first show that Bolzano--Weierstra\ss{} compactness implies an instance of excluded middle
known as the \define{limited principle of omniscience}:
\indexsee{axiom!limited principle of omniscience}{limited principle of omniscience}%
\indexdef{limited principle of omniscience}%
for every $\alpha : \N \to \bool$,
%
\begin{equation} \label{eq:lpo}
  \Parens{\sm{n : \N} \alpha(n) = \btrue} +
  \Parens{\prd{n : \N} \alpha(n) = \bfalse}.
\end{equation}
%
Computationally speaking, we would not expect this principle to hold, because it asks us to decide
whether infinitely many values of a function are~$\bfalse$.

\begin{thm} \label{analysis-bw-lpo}
  %
  Bolzano--Weierstra\ss{} compactness of $[0,1]$ implies the limited principle of omniscience.
  \index{compactness!Bolzano--Weierstrass@Bolzano--Weierstra\ss{}}%
\end{thm}

\begin{proof}
  Given any $\alpha : \N \to \bool$, define the sequence\index{sequence} $x : \N \to [0,1]$ by
  %
  \begin{equation*}
    x_n \defeq
    \begin{cases}
      0 & \text{if $\alpha(k) = \bfalse$ for all $k < n$,}\\
      1 & \text{if $\alpha(k) = \btrue$ for some $k < n$}.
    \end{cases}
  \end{equation*}
  %
  If the Bolzano--Weierstra\ss{} property holds, there exists a strictly increasing $f : \N \to
  \N$ such that $x \circ f$ is a Cauchy sequence\index{Cauchy!sequence}. For a sufficiently large $n :
  \N$ the $n$-th term $x_{f(n)}$ is within $1/6$ of its limit. Either $x_{f(n)} < 2/3$ or
  $x_{f(n)} > 1/3$. If $x_{f(n)} < 2/3$ then~$x_n$ converges to $0$ and so $\prd{n : \N}
  \alpha(n) = \bfalse$. If $x_{f(n)} > 1/3$ then $x_{f(n)} = 1$, therefore $\sm{n : \N}
  \alpha(n) = \btrue$.
\end{proof}

While we might not mourn Bolzano--Weierstra\ss{} compactness too much, it seems harder to live
without Heine--Borel compactness, as attested by the fact that both classical mathematics
and Brouwer's Intuitionism accepted it. As we do not want to wade too deeply into general
topology, we shall work with basic open sets. In the case of $\R$ these are the open
intervals with rational endpoints. A family of such intervals, indexed by a type~$I$,
would be a map
%
\begin{equation*}
  \mathcal{F} : I \to \setof{(q, r) : \Q \times \Q | q < r},
\end{equation*}
%
with the idea that a pair of rationals $(q, r)$ with $q < r$ determines the type $\setof{ x : \R | q < x < r}$. It is slightly more convenient to allow degenerate intervals as well, so we take a
\define{family of basic intervals}
\indexdef{family!of basic intervals}%
\indexdef{interval!family of basic}%
to be a map
%
\begin{equation*}
  \mathcal{F} : I \to \Q \times \Q.
\end{equation*}
%
To be quite precise, a family is a dependent pair $(I, \mathcal{F})$, not just
$\mathcal{F}$. A \define{finite family of basic intervals} is one indexed by $\setof{ m :
  \N | m < n}$ for some $n : \N$. We usually present it by a finite list $[(q_0, r_0), \ldots,
(q_{n-1}, r_{n-1})]$. Finally, a \define{finite subfamily}\indexdef{subfamily, finite, of intervals} of $(I, \mathcal{F})$ is given
by a list of indices $[i_1, \ldots, i_n]$ which then determine the finite family
$[\mathcal{F}(i_1), \ldots, \mathcal{F}(i_n)]$.

As long as we are aware of the distinction between a pair $(q, r)$ and the corresponding
interval $\setof{ x : \R | q < x < r}$, we may safely use the same notation $(q, r)$ for
both. Intersections\indexdef{intersection!of intervals} and inclusions\indexdef{inclusion!of intervals}\indexdef{containment!of intervals} of intervals are expressible in terms of their
endpoints:
%
\symlabel{interval-intersection}
\symlabel{interval-subset}
\begin{align*}
  (q, r) \cap (s, t) &\ \defeq\  (\max(q, s), \min(r, t)),\\
  (q, r) \subseteq (s, t) &\ \defeq\ (q < r \Rightarrow s \leq q < r \leq t).
\end{align*}
%
We say that $\intfam{i}{I}{(q_i, r_i)}$ \define{(pointwise) covers $[a,b]$}
\indexdef{interval!pointwise cover}%
\indexdef{cover!pointwise}%
\indexdef{pointwise!cover}%
when
%
\begin{equation} \label{eq:cover-pointwise-truncated}
  \fall{x : [a,b]} \exis{i : I} q_i < x < r_i.
\end{equation}
%
The \define{Heine--Borel compactness for $[0,1]$}
\indexdef{compactness!Heine--Borel}%
states that every covering family of $[0,1]$
merely has a finite subfamily which still covers $[0,1]$.

\index{depression}
\begin{thm} \label{classical-Heine-Borel}
  \index{excluded middle}%
  If excluded middle holds then $[0,1]$ is Heine--Borel compact.
\end{thm}

\begin{proof}
  Assume for the purpose of reaching a contradiction that a family $\intfam{i}{I}{(a_i,
    b_i)}$ covers $[0,1]$ but no finite subfamily does. We construct a sequence of closed
  intervals $[q_n, r_n]$ which are nested, their sizes shrink to~$0$, and none of them is covered
  by a finite subfamily of $\intfam{i}{I}{(a_i, b_i)}$.

  We set $[q_0, r_0] \defeq [0,1]$. Assuming $[q_n, r_n]$ has been constructed, let $s
  \defeq (2 q_n + r_n)/3$ and $t \defeq (q_n + 2 r_n)/3$. Both $[q_n, t]$ and $[s, r_n]$
  are covered by $\intfam{i}{I}{(a_i, b_i)}$, but they cannot both have a finite subcover,
  or else so would $[q_n, r_n]$. Either $[q_n, t]$ has a finite subcover or it does not.
  If it does we set $[q_{n+1}, r_{n+1}] \defeq [s, r_n]$, otherwise we set $[q_{n+1},
  r_{n+1}] \defeq [q_n, t]$.

  The sequences $q_0, q_1, \ldots$ and $r_0, r_1, \ldots$ are both Cauchy and they
  converge to a point $x : [0,1]$ which is contained in every $[q_n, r_n]$.
  There merely exists $i : I$ such that $a_i < x < b_i$. Because the sizes of the
  intervals $[q_n, r_n]$ shrink to zero, there is $n : \N$ such that $a_i < q_n \leq x
  \leq r_n < b_i$, but this means that $[q_n, r_n]$ is covered by a single interval $(a_i,
  b_i)$, while at the same time it has no finite subcover. A contradiction.
\end{proof}

Without excluded middle, or a pinch of Brouwerian Intuitionism, we seem to be stuck.
Nevertheless, Heine--Borel compactness of $[0,1]$ \emph{can} be recovered in a constructive
setting, in a fashion that is still compatible with classical mathematics! For this to be
done, we need to revisit the notion of cover. The trouble with
\eqref{eq:cover-pointwise-truncated} is that the truncated existential allows a space to
be covered in any haphazard way, and so computationally speaking, we stand no chance of
merely extracting a finite subcover. By removing the truncation we get
%
\begin{equation} \label{eq:cover-pointwise}
  \prd{x : [0,1]} \sm{i : I} q_i < x < r_i,
\end{equation}
%
which might help, were it not too demanding of covers. With this definition we
could not even show that $(0,3)$ and $(2,5)$ cover $[1,4]$ because that would amount
to exhibiting a non-constant map $[1,4] \to \bool$, see
\cref{ex:reals-non-constant-into-Z}.  Here we can take a lesson from ``pointfree topology''
\index{pointfree topology}%
\index{topology!pointfree}%
(i.e.\ locale theory):
\index{locale}%
the notion of cover ought to be expressed in terms of open sets, without
reference to points. Such a ``holistic'' view of space will then allow us to analyze the
notion of cover, and we shall be able to recover Heine--Borel compactness.  Locale
theory uses power sets,
\index{power set}%
which we could obtain by assuming propositional resizing;
\index{propositional!resizing}%
but instead we can steal ideas from the predicative cousin of locale theory,
\index{mathematics!predicative}%
which is called ``formal topology''.
\index{formal!topology}%

\index{acceptance|(}

Suppose that we have a family $\pairr{I, \mathcal{F}}$ and an interval $(a, b)$. How might
we express the fact that $(a,b)$ is covered by the family, without referring to points?
Here is one: if $(a, b)$ equals some $\mathcal{F}(i)$ then it is covered by the family.
And another one: if $(a,b)$ is covered by some other family $(J, \mathcal{G})$, and in
turn each $\mathcal{G}(j)$ is covered by $\pairr{I, \mathcal{F}}$, then $(a,b)$ is covered
$\pairr{I, \mathcal{F}}$. Notice that we are listing \emph{rules} which can be used to
\emph{deduce} that $\pairr{I, \mathcal{F}}$ covers $(a,b)$. We should find sufficiently
good rules and turn them into an inductive definition.

\begin{defn} \label{defn:inductive-cover}
  %
  The \define{inductive cover $\cover$}
  \indexdef{inductive!cover}%
  \indexdef{cover!inductive}%
  is a mere relation
  %
  \begin{equation*}
    {\cover} : (\Q \times \Q) \to \Parens{\sm{I : \type} (I \to \Q \times \Q)} \to \prop
  \end{equation*}
  %
  defined inductively by the following rules, where $q, r, s, t$ are rational numbers and
  $\pairr{I, \mathcal{F}}$, $\pairr{J, \mathcal{G}}$ are families of basic intervals:
  %
  \begin{enumerate}

  \item \emph{reflexivity:}
    \index{reflexivity!of inductive cover}%
    $\mathcal{F}(i) \cover \pairr{I, \mathcal{F}}$ for all $i : I$,

  \item \emph{transitivity:}
    \index{transitivity!of inductive cover}%
    if $(q, r) \cover \pairr{J, \mathcal{G}}$ and $\fall{j : J} \mathcal{G}(j) \cover \pairr{I,\mathcal{F}}$
    then $(q, r) \cover \pairr{I, \mathcal{F}}$,

  \item \emph{monotonicity:}
    \index{monotonicity!of inductive cover}%
    if $(q, r) \subseteq (s, t)$ and $(s,t) \cover \pairr{I, \mathcal{F}}$ then $(q, r) \cover
    \pairr{I, \mathcal{F}}$,

  \item \emph{localization:}
    \index{localization of inductive cover}%
    if $(q, r) \cover (I, \mathcal{F})$ then $(q, r) \cap (s, t) \cover
    \intfam{i}{I}{(\mathcal{F}(i) \cap (s, t))}$.

  \item \label{defn:inductive-cover-interval-1}
    if $q < s < t < r$ then $(q, r) \cover [(q, t), (r, s)]$,

  \item \label{defn:inductive-cover-interval-2}
    $(q, r) \cover \intfam{u}{\setof{ (s,t) : \Q \times \Q | q < s < t < r}}{u}$.
  \end{enumerate}
\end{defn}

The definition should be read as a higher-inductive type in which the listed rules are
point constructors, and the type is $(-1)$-truncated. The first four clauses are of a
general nature and should be intuitively clear. The last two clauses are specific to the
real line: one says that an interval may be covered by two intervals if they overlap,
while the other one says that an interval may be covered from within. Incidentally, if $r
\leq q$ then $(q, r)$ is covered by the empty family by the last clause.

Inductive covers enjoy the Heine--Borel property, the proof of which requires a lemma.

\begin{lem} \label{reals-formal-topology-locally-compact}
  Suppose $q < s < t < r$ and $(q, r) \cover \pairr{I, \mathcal{F}}$. Then there merely
  exists a finite subfamily of $\pairr{I, \mathcal{F}}$ which inductively covers $(s, t)$.
\end{lem}

\begin{proof}
  We prove the statement by induction on $(q, r) \cover \pairr{I, \mathcal{F}}$. There are
  six cases:
  %
  \begin{enumerate}

  \item Reflexivity: if $(q, r) = \mathcal{F}(i)$ then by monotonicity $(s, t)$ is covered
    by the finite subfamily $[\mathcal{F}(i)]$.

  \item Transitivity:
    suppose $(q, r) \cover \pairr{J, \mathcal{G}}$ and $\fall{j : J} \mathcal{G}(j) \cover
    \pairr{I, \mathcal{F}}$. By the inductive hypothesis there merely exists
    $[\mathcal{G}(j_1), \ldots, \mathcal{G}(j_n)]$ which covers $(s, t)$.
    Again by the inductive hypothesis, each of $\mathcal{G}(j_k)$ is covered by a finite
    subfamily of $\pairr{I, \mathcal{F}}$, and we can collect these into a finite
    subfamily which covers $(s, t)$.

  \item Monotonicity:
    if $(q, r) \subseteq (u, v)$ and $(u, v) \cover \pairr{I, \mathcal{F}}$ then we may
    apply the inductive hypothesis to $(u, v) \cover \pairr{I, \mathcal{F}}$ because $u <
    s < t < v$.

  \item Localization:
    suppose $(q', r') \cover \pairr{I, \mathcal{F}}$ and $(q, r) = (q', r') \cap (a, b)$.
    Because $q' < s < t < r'$, by the inductive hypothesis there is a finite subcover
    $[\mathcal{F}(i_1), \ldots, \mathcal{F}(i_n)]$ of $(s, t)$. We also know that $a < s <
    t < b$, therefore $(s, t) = (s, t) \cap (a, b)$ is covered by
    $[\mathcal{F}(i_1) \cap (a,b), \ldots, \mathcal{F}(i_n) \cap (a,b)]$, which is a
    finite subfamily of $\intfam{i}{I}{(\mathcal{F}(i) \cap (a, b))}$.

  \item If $(q, r) \cover [(q, v), (u, r)]$ for some $q < u < v < r$ then by monotonicity
    $(s, t) \cover [(q, v), (u, r)]$.

  \item Finally, $(s, t) \cover \intfam{z}{\setof{ (u,v):\Q \times \Q | q < u < v < r}}{z}$ by
    reflexivity. \qedhere
  \end{enumerate}
\end{proof}

Say that \define{$\pairr{I, \mathcal{F}}$ inductively covers
  $[a, b]$} when there merely exists $\epsilon : \Qp$ such that $(a - \epsilon, b +
\epsilon) \cover \pairr{I, \mathcal{F}}$.

\begin{cor} \label{interval-Heine-Borel}
  \index{compactness!Heine-Borel}%
  \index{interval!open and closed}%
  A closed interval is Heine--Borel compact for inductive covers.
\end{cor}

\begin{proof}
  Suppose $[a, b]$ is inductively covered by $\pairr{I, \mathcal{F}}$, so there merely is
  $\epsilon : \Qp$ such that $(a - \epsilon, b + \epsilon) \cover \pairr{I, \mathcal{F}}$.
  By \cref{reals-formal-topology-locally-compact} there is a finite subcover of
  $(a - \epsilon/2, b + \epsilon/2)$, which is therefore a finite subcover of $[a, b]$.
\end{proof}

Experience from formal topology\index{topology!formal} shows that the rules for inductive covers are sufficient
for a constructive development of pointfree topology. But we can also provide our own
evidence that they are a reasonable notion.

\begin{thm} \label{inductive-cover-classical}
  \mbox{}
  %
  \begin{enumerate}
  \item An inductive cover is also a pointwise cover.
  \item Assuming excluded middle, a pointwise cover is also an inductive cover.
  \end{enumerate}
\end{thm}

\begin{proof}
  \mbox{}
  %
  \begin{enumerate}

  \item
    Consider a family of basic intervals $\pairr{I, \mathcal{F}}$, where we write $(q_i,
    r_i) \defeq \mathcal{F}(i)$, an interval $(a,b)$ inductively covered by $\pairr{I,
      \mathcal{F}}$, and $x$ such that $a < x < b$.
    %
    We prove by induction on $(a,b) \cover \pairr{I, \mathcal{F}}$ that there merely
    exists $i : I$ such that $q_i < x < r_i$. Most cases are pretty obvious, so we show
    just two. If $(a,b) \cover \pairr{I, \mathcal{F}}$ by reflexivity, then there merely
    is some $i : I$ such that $(a,b) = (q_i, r_i)$ and so $q_i < x < r_i$. If $(a,b)
    \cover \pairr{I, \mathcal{F}}$ by transitivity via $\intfam{j}{J}{(s_j, t_j)}$ then by
    the inductive hypothesis there merely is $j : J$ such that $s_j < x < t_j$, and then since
    $(s_j, t_j) \cover \pairr{I, \mathcal{F}}$ again by the inductive hypothesis there merely
    exists $i : I$ such that $q_i < x < r_i$. Other cases are just as exciting.

  \item Suppose $\intfam{i}{I}{(q_i, r_i)}$ pointwise covers $(a, b)$. By
    \cref{defn:inductive-cover-interval-2} of \cref{defn:inductive-cover} it
    suffices to show that $\intfam{i}{I}{(q_i, r_i)}$ inductively covers $(c, d)$ whenever
    $a < c < d < b$, so consider such $c$ and $d$. By \cref{classical-Heine-Borel}
    there is a finite subfamily $[i_1, \ldots, i_n]$ which already pointwise covers $[c,
    d]$, and hence $(c,d)$. Let $\epsilon : \Qp$ be a Lebesgue number
    \index{Lebesgue number}
    for $(q_{i_1}, r_{i_1}), \ldots, (q_{i_n}, r_{i_n})$ as in
    \cref{ex:finite-cover-lebesgue-number}. There is a positive $k : \N$ such that $2 (d - c)/k
    < \min(1, \epsilon)$. For $0 \leq i \leq k$ let
    %
    \begin{equation*}
      c_k \defeq ((k - i) c + i d) / k.
    \end{equation*}
    %
    The intervals $(c_0, c_2)$, $(c_1, c_3)$, \dots, $(c_{k-2}, c_k)$ inductively cover
    $(c,d)$ by repeated use of transitivity and~\cref{defn:inductive-cover-interval-1}
    in \cref{defn:inductive-cover}. Because their widths are below $\epsilon$ each of
    them is contained in some $(q_i, r_i)$, and we may use transitivity and monotonicity to
    conclude that $\intfam{i}{I}{(q_i, r_i)}$ inductively cover $(c, d)$. \qedhere
  \end{enumerate}
\end{proof}

The upshot of the previous theorem is that, as far as classical mathematics is concerned,
there is no difference between a pointwise and an inductive cover. In particular, since it
is consistent to assume excluded middle in homotopy type theory, we cannot exhibit an
inductive cover which fails to be a pointwise cover. Or to put it in a different way, the
difference between pointwise and inductive covers is not what they cover but in the
\emph{proofs} that they cover.

We could write another book by going on like this, but let us stop here and hope that we
have provided ample justification for the claim that analysis can be developed in homotopy
type theory. The curious reader should consult \cref{ex:mean-value-theorem} for
constructive versions of the mean value theorem.

\index{acceptance|)}

\index{mathematics!classical|)}%
\index{mathematics!constructive|)}%

\section{The surreal numbers}
\label{sec:surreals}

\index{surreal numbers|(}%

In this section we consider another example of a higher inductive-in\-duc\-tive type, which draws together many of our threads: Conway's field \NO of \emph{surreal numbers}~\cite{conway:onag}.
The surreal numbers are the natural common generalization of the (Dedekind) real numbers (\cref{sec:dedekind-reals}) and the ordinal numbers (\cref{sec:ordinals}).
Conway, working in classical\index{mathematics!classical} mathematics with excluded middle and Choice, defines a surreal number to be a pair of \emph{sets} of surreal numbers, written $\surr L R$, such that every element of $L$ is strictly less than every element of $R$.
This obviously looks like an inductive definition, but there are three issues with regarding it as such.

Firstly, the definition requires the relation of (strict) inequality between surreals, so that relation must be defined simultaneously with the type \NO of surreals.
(Conway avoids this issue by first defining \emph{games}\index{game!Conway}, which are like surreals but omit the compatibility condition on $L$ and $R$.)
As with the relation $\closesym$ for the Cauchy reals, this simultaneous definition could \emph{a priori} be either inductive-inductive or inductive-recursive.
We will choose to make it inductive-inductive, for the same reasons we made that choice for $\closesym$.

Moreover, we will define strict inequality $<$ and non-strict inequality $\le$ for surreals separately (and mutually inductively).
Conway defines $<$ in terms of $\le$, in a way which is sensible classically but not constructively.
\index{mathematics!constructive}%
Furthermore, a negative definition of $<$ would make it unacceptable as a hypothesis of the constructor of a higher inductive type (see \cref{sec:strictly-positive}).

Secondly, Conway says that $L$ and $R$ in $\surr L R$ should be ``sets of surreal numbers'', but the naive meaning of this as a predicate $\NO\to\prop$ is not positive, hence cannot be used as input to an inductive constructor.
However, this would not be a good type-theoretic translation of what Conway means anyway, because in set theory the surreal numbers form a proper class, whereas the sets $L$ and $R$ are true (small) sets, not arbitrary subclasses of \NO.
In type theory, this means that \NO will be defined relative to a universe \UU, but will itself belong to the next higher universe $\UU'$, like the sets \ord and \card of ordinals and cardinals, the cumulative hierarchy $V$, or even the Dedekind reals in the absence of propositional resizing.
\index{propositional!resizing}%
We will then require the ``sets'' $L$ and $R$ of surreals to be \UU-small, and so it is natural to represent them by \emph{families} of surreals indexed by some \UU-small type.
(This is all exactly the same as what we did with the cumulative hierarchy in \cref{sec:cumulative-hierarchy}.)
That is, the constructor of surreals will have type
\[ \prd{\LL,\RR:\UU} (\LL\to\NO) \to (\RR\to \NO) \to (\text{some condition}) \to \NO \]
which is indeed strictly positive.\index{strict!positivity}

Finally, after giving the mutual definitions of \NO and its ordering, Conway declares two surreal numbers $x$ and $y$ to be \emph{equal} if $x\le y$ and $y\le x$.
This is naturally read as passing to a quotient of the set of ``pre-surreals'' by an equivalence relation.
%(In set-theoretic foundations, one has to us an additional trick to deal with large equivalence classes.)
However, in the absence of the axiom of choice, such a quotient presents the same problem as the quotient in the usual construction of Cauchy reals: it will no longer be the case that a pair of families \emph{of surreals} yield a new surreal $\surr L R$, since we cannot necessarily ``lift'' $L$ and $R$ to families of pre-surreals.
Of course, we can solve this problem in the same way we did for Cauchy reals, by using a \emph{higher} inductive-inductive definition.

\begin{defn}\label{defn:surreals}
  The type \NO of \define{surreal numbers},
  \indexdef{surreal numbers}%
  \indexsee{number!surreal}{surreal numbers}%
  along with the relations $\mathord<:\NO\to\NO\to\type$ and $\mathord\le:\NO\to\NO\to\type$, are defined higher inductive-inductively as follows.
  The type \NO has the following constructors.
  \begin{itemize}
  \item For any $\LL,\RR:\UU$ and functions $\LL\to \NO$ and $\RR\to \NO$, whose values we write as $x^L$ and $x^R$ for $L:\LL$ and $R:\RR$ respectively, if $\fall{L:\LL}{R:\RR} x^L<x^R$, then there is a surreal number $x$.
  \item For any $x,y:\NO$ such that $x\le y$ and $y\le x$, we have $\noeq(x,y):x=y$.
  \end{itemize}
  We will refer to the inputs of the first constructor as a \define{cut}.
  \indexdef{cut!of surreal numbers}%
  If $x$ is the surreal number constructed from a cut, then the notation $x^L$ will implicitly assume $L:\LL$, and similarly $x^R$ will assume $R:\RR$.
  In this way we can usually avoid naming the indexing types $\LL$ and $\RR$, which is convenient when there are many different cuts under discussion.
  Following Conway, we call $x^L$ a \emph{left option}\indexdef{option of a surreal number} of $x$ and $x^R$ a \emph{right option}.

  The path constructor implies that different cuts can define the same surreal number.
  Thus, it does not make sense to speak of the left or right options of an arbitrary surreal number $x$, unless we also know that $x$ is defined by a particular cut.
  Thus in what follows we will say, for instance, ``given a cut defining a surreal number $x$'' in contrast to ``given a surreal number $x$''.

  The relation $\le$ has the following constructors.
  \index{non-strict order}%
  \index{order!non-strict}%
  \begin{itemize}
  \item Given cuts defining two surreal numbers $x$ and $y$, if $x^L<y$ for all $L$, and $x<y^R$ for all $R$, then $x\le y$.
  \item Propositional truncation:
    for any $x,y:\NO$, if $p,q:x\le y$, then $p=q$.
  \end{itemize}
  And the relation $<$ has the following constructors.
  \index{strict!order}%
  \index{order!strict}%
  \begin{itemize}
    % Don't technically need x in the first one and y in the second one to be defined by cuts?
  \item Given cuts defining two surreal numbers $x$ and $y$, if there is an $L$ such that $x\le y^L$, then $x<y$.
  \item Given cuts defining two surreal numbers $x$ and $y$, if there is an $R$ such that $x^R\le y$, then $x<y$.
  \item Propositional truncation: for any $x,y:\NO$, if $p,q:x<y$, then $p=q$.
  \end{itemize}
\end{defn}

\noindent
We compare this with Conway's definitions:
\begin{itemize}\footnotesize
\item[-] If $L,R$ are any two sets of numbers, and no member of $L$ is $\ge$ any member of $R$, then there is a number $\surr L R$.
  All numbers are constructed in this way.
\item[-] $x\ge y$ iff (no $x^R\le y$ and $x\le$ no $y^L$).
\item[-] $x=y$ iff ($x \ge y$ and $y\ge x$).
\item[-] $x>y$ iff ($x\ge y$ and $y\not\ge x$).
\end{itemize}
The inclusion of $x\ge y$ in the definition of $x>y$ is unnecessary if all objects are [surreal] numbers rather than ``games''\index{game!Conway}.
Thus, Conway's $<$ is just the negation of his $\ge$, so that his condition for $\surr L R$ to be a surreal is the same as ours.
Negating Conway's $\le$ and canceling double negations, we arrive at our definition of $<$, and we can then reformulate his $\le$ in terms of $<$ without negations.

We can immediately populate $\NO$ with many surreal numbers.
Like Conway, we write
\symlabel{surreal-cut}
\[\surr{x,y,z,\dots}{u,v,w,\dots}\]
for the surreal number defined by a cut where $\LL\to\NO$ and $\RR\to\NO$ are families described by $x,y,z,\dots$ and $u,v,w,\dots$.
Of course, if $\LL$ or $\RR$ are $\emptyt$, we leave the corresponding part of the notation empty.
There is an unfortunate clash with the standard notation $\setof{x:A | P(x)}$ for subsets, but we will not use the latter in this section.
\begin{itemize}
\item We define $\iota_{\nat}:\nat\to\NO$ recursively by
  \begin{align*}
    \iota_{\nat}(0) &\defeq \surr{}{},\\
    \iota_\nat(\suc(n)) &\defeq \surr{\iota_\nat(n)}{}.
  \end{align*}
  That is, $\iota_\nat(0)$ is defined by the cut consisting of $\emptyt\to\NO$ and $\emptyt\to\NO$.
  Similarly, $\iota_\nat(\suc(n))$ is defined by $\unit\to\NO$ (picking out $\iota_\nat(n)$) and $\emptyt\to\NO$.
\item Similarly, we define $\iota_{\Z}:\Z\to\NO$ using the sign-case recursion principle (\cref{thm:sign-induction}):
  \begin{align*}
    \iota_{\Z}(0) &\defeq \surr{}{},\\
    \iota_\Z(n+1) &\defeq \surr{\iota_\Z(n)}{} & &\text{$n\ge 0$,}\\
    \iota_\Z(n-1) &\defeq \surr{}{\iota_\Z(n)} & &\text{$n\le 0$.}
  \end{align*}
\item By a \define{dyadic rational}
  \indexdef{rational numbers!dyadic}%
  \indexsee{dyadic rational}{rational numbers, dyadic}%
  we mean a pair $(a,n)$ where $a:\Z$ and $n:\nat$, and such that if $n>0$ then $a$ is odd.
  We will write it as $a/2^n$, and identify it with the corresponding rational number.
  If $\Q_D$ denotes the set of dyadic rationals, we define $\iota_{\Q_D}:\Q_D\to\NO$ by induction on $n$:
  \begin{align*}
    \iota_{\Q_D}(a/2^0) &\defeq \iota_\Z(a),\\
    \iota_{\Q_D}(a/2^n) &\defeq \surr{a/2^n - 1/2^n}{a/2^n + 1/2^n},
    \quad \text{for $n>0$.}
  \end{align*}
  Here we use the fact that if $n>0$ and $a$ is odd, then $a/2^n \pm 1/2^n$ is a dyadic rational with a smaller denominator than $a/2^n$.
\item We define $\iota_{\RD}:\RD\to\NO$,\label{reals-into-surreals} where $\RD$ is (any version of) the Dedekind reals from \cref{sec:dedekind-reals}, by
  \begin{align*}
    \iota_{\RD}(x) &\defeq
    \surr{q\in\Q_D \text{ such that } q<x}{q\in\Q_D \text{ such that } x<q}.
  \end{align*}
  Unlike in the previous cases, it is not obvious that this extends $\iota_{\Q_D}$ when we regard dyadic rationals as Dedekind reals.
  This follows from the simplicity theorem (\cref{thm:NO-simplicity}).
\item Recall the type \ord of \emph{ordinals}\index{ordinal} from \cref{sec:ordinals}, which is well-ordered by the relation $<$, where $A<B$ means that $A = \ordsl B b$ for some $b:B$.
  We define $\iota_{\ord}:\ord\to\NO$\label{ord-into-surreals} by well-founded recursion (\cref{thm:wfrec}) on $\ord$:
  \begin{equation*}
    \iota_{\ord}(A) \defeq
    \surr{\iota_\ord(\ordsl A a) \text{ for all } a:A}{}.
  \end{equation*}
  It will also follow from the simplicity theorem that $\iota_\ord$ restricted to finite ordinals agrees with $\iota_\nat$.
  (We caution the reader, however, that unlike the above examples, $\iota_\ord$ is not constructively injective unless we restrict it to a smaller class of ordinals; see \cref{ex:ord-into-surreals,ex:hiit-plump}.)
\item A few more interesting examples taken from Conway:
  \begin{align*}
    \omega &\defeq \surr{0,1,2,3,\dots}{} \qquad\text{(also an ordinal)}\\
    -\omega &\defeq \surr{}{\dots,-3,-2,-1,0}\\
    1/\omega &\defeq \textstyle\surr{0}{1,\frac12,\frac14,\frac18,\dots}\\
    \omega-1 &\defeq \surr{0,1,2,3,\dots}{\omega}\\
    \omega/2 &\defeq \surr{0,1,2,3,\dots}{\dots,\omega-2,\omega-1,\omega}.
  \end{align*}
\end{itemize}

In identifying surreal numbers presented by different cuts, the following simple observation is useful.

\begin{thm}[Conway's simplicity theorem]\label{thm:NO-simplicity}
  \index{simplicity theorem}%
  \index{theorem!Conway's simplicity}%
  Suppose $x$ and $z$ are surreal numbers defined by cuts, and that the following hold.
  \begin{itemize}
  \item $x^L < z < x^R$ for all $L$ and $R$.
  \item For every left option $z^L$ of $z$, there exists a left option $x^{L'}$ with $z^L\le x^{L'}$.
  \item For every right option $z^R$ of $z$, there exists a right option $x^{R'}$ with $x^{R'}\le z^R$.
  \end{itemize}
  Then $x=z$.
\end{thm}
\begin{proof}
  Applying the path constructor of $\NO$, we must show $x\le z$ and $z\le x$.
  The first entails showing $x^L<z$ for all $L$, which we assumed, and $x<z^R$ for all $R$.
  But by assumption, for any $z^R$ there is an $x^{R'}$ with $x^{R'}\le z^R$ hence $x<z^R$ as desired.
  Thus $x\le z$; the proof of $z\le x$ is symmetric.
\end{proof}

\index{induction principle!for surreal numbers}
In order to say much more about surreal numbers, however, we need their induction principle.
The mutual induction principle for $(\NO,\le,<)$ applies to three families of types:
\begin{align*}
  A &: \NO\to\type\\
  B &: \prd{x,y:\NO}{a:A(x)}{b:A(y)} (x\le y) \to \type\\
  C &: \prd{x,y:\NO}{a:A(x)}{b:A(y)} (x<y) \to \type.
\end{align*}
As with the induction principle for Cauchy reals, it is helpful to think of $B$ and $C$ as families of relations between the types $A(x)$ and $A(y)$.
\symlabel{NO-recursion}
Thus we write $B(x,y,a,b,\xi)$ as $(x,a) \ble^\xi (y,b)$ and $C(x,y,a,b,\xi)$ as $(x,a) \blt^\xi (y,b)$.
Similarly, we usually omit the $\xi$ since it inhabits a mere proposition and so is uninteresting, and we may often omit $x$ and $y$ as well, writing simply $a\ble b$ or $a\blt b$.
With these notations, the hypotheses of the induction principle are the following.
\begin{itemize}
\item For any cut defining a surreal number $x$, together with
  \begin{enumerate}
  \item for each $L$, an element $a^L:A(x^L)$, and
  \item for each $R$, an element $a^R:A(x^R)$, such that
  \item for all $L$ and $R$ we have $(x^L,a^L) \blt (x^R,a^R)$
  \end{enumerate}
  there is a specified element $f_a:A(x)$.
  We call such data a \define{dependent cut}
  \indexdef{cut!of surreal numbers!dependent}%
  \indexdef{dependent!cut}%
  over the cut defining~$x$.
\item For any $x,y:\NO$ with $a:A(x)$ and $b:A(y)$, if $x\le y$ and $y\le x$ and also $(x,a) \ble (y,b)$
  and $(y,b) \ble (x,a)$,
  then $\dpath{A}{\noeq}{a}{b}$.
\item Given cuts defining two surreal numbers $x$ and $y$, and dependent cuts $a$ over $x$ and $b$ over $y$, such that for all $L$ we have $x^L<y$ and $(x^L,a^L)\blt (y,f_b)$,
  and for all $R$ we have $x<y^R$ and $(x,f_a) \blt (y^R,b^R)$,
  then $(x,f_a) \ble (y,f_b)$.
\item $\ble$ takes values in mere propositions.
\item Given cuts defining two surreal numbers $x$ and $y$, dependent cuts $a$ over $x$ and $b$ over $y$, and an $L_0$ such that $x\le y^{L_0}$ and $(x,f_a) \ble (y^{L_0},b^{L_0})$,
  we have $(x,f_a) \blt (y,f_b)$.
\item Given cuts defining two surreal numbers $x$ and $y$, dependent cuts $a$ over $x$ and $b$ over $y$, and an ${R_0}$ such that $x^{R_0}\le y$ together with $(x^{R_0},a^{R_0}),\ble (y,f_b)$,
  we have $(x,f_a) \blt (y,f_b)$.
\item $\blt$ takes values in mere propositions.
\end{itemize}
Under these hypotheses we deduce a function $f:\prd{x:\NO} A(x)$ such that
\begin{align}
  f(x) &\;\jdeq\; f_{f[x]} \label{eq:noind1}\\
  (x\le y) &\;\Rightarrow\; (x,f(x)) \ble (y,f(y)) \notag\\
  (x< y) &\;\Rightarrow\; (x,f(x)) \blt (y,f(y)). \notag
\end{align}
In the computation rule~\eqref{eq:noind1} for the point constructor, $x$ is a surreal number defined by a cut, and $f[x]$ denotes the dependent cut over $x$ defined by applying $f$ (and using the fact that $f$ takes $<$ to $\blt$).
As usual, we will generally use pattern-matching notation, where the definition of $f$ on a cut $\surr{x^L}{x^R}$ may use the symbols $f(x^L)$ and $f(x^R)$ and the assumption that they form a dependent cut.

As with the Cauchy reals, we have special cases resulting from trivializing some of $A$, $\ble$, and~$\blt$.
Taking $\ble$ and $\blt$ to be constant at \unit, we have \define{\NO-induction}, which for simplicity we state only for mere properties:
\begin{itemize}
\item Given $P:\NO\to\prop$, if $P(x)$ holds whenever $x$ is a surreal number defined by a cut such that $P(x^L)$ and $P(x^R)$ hold for all
$L$ and $R$, then $P(x)$ holds for all $x:\NO$.
\end{itemize}
This should be compared with Conway's remark:
\begin{quote}\footnotesize
  In general when we wish to establish a proposition $P(x)$ for all numbers $x$, we will prove it inductively by deducing $P(x)$ from the truth of all the propositions $P(x^L)$ and $P(x^R)$.
  We regard the phrase ``all numbers are constructed in this way'' as justifying the legitimacy of this procedure.
\end{quote}
With $\NO$-induction, we can prove

\begin{thm}[Conway's Theorem 0]\label{thm:NO-refl-opt}\
  \index{theorem!Conway's 0}%
  \begin{enumerate}
  \item For any $x:\NO$, we have $x\le x$.\label{item:NO-le-refl}
  \item For any $x:\NO$ defined by a cut, we have $x^L <x$ and $x<x^R$ for all $L$ and $R$.\label{item:NO-lt-opt}
  \end{enumerate}
\end{thm}
\begin{proof}
  Note first that if $x\le x$, then whenever $x$ occurs as a left option of some cut $y$, we have $x<y$ by the first constructor of $<$, and similarly whenever $x$ occurs as a right option of a cut $y$, we have $y<x$ by the second constructor of $<$.
  In particular,~\ref{item:NO-le-refl}$\Rightarrow$\ref{item:NO-lt-opt}.

  We prove~\ref{item:NO-le-refl} by $\NO$-induction on $x$.
  Thus, assume $x$ is defined by a cut such that $x^L\le x^L$ and $x^R \le x^R$ for all $L$ and $R$.
  But by our observation above, these assumptions imply $x^L<x$ and $x<x^R$ for all $L$ and $R$, yielding $x\le x$ by the constructor of $\le$.
\end{proof}

\begin{cor}\label{thm:NO-set}
  \NO is a 0-type.
%  (As with $V$, it might be confusing to say that it is a ``set''.)
\end{cor}
\begin{proof}
  The mere relation $R(x,y)\defeq (x\le y) \land (y\le x)$ implies identity by the path constructor of $\NO$, and contains the diagonal by \cref{thm:NO-refl-opt}\ref{item:NO-le-refl}.
  Thus, \cref{thm:h-set-refrel-in-paths-sets} applies.
\end{proof}

By contrast, Conway's Theorem 1 (transitivity of $\le$) is somewhat harder to establish with our definition; see \cref{thm:NO-unstrict-transitive}.

% Of course, we also have:

% \begin{lem}
%   Every surreal number is merely defined by a cut.
% \end{lem}
% \begin{proof}
%   Obvious by $\NO$-induction.
% \end{proof}

We will also need the joint recursion principle, \define{$(\NO,\le,<)$-recursion}.
It is convenient to state this as follows.
Suppose $A$ is a type equipped with relations $\mathord\ble:A\to A\to\prop$ and $\mathord\blt:A\to A\to\prop$.
Then we can define $f:\NO\to A$ by doing the following.
\begin{enumerate}
\item For any $x$ defined by a cut, assuming $f(x^L)$ and $f(x^R)$ to be defined such that $f(x^L)\blt f(x^R)$ for all $L$ and $R$, we must define $f(x)$.  (We call this the \emph{primary clause} of the recursion.)\label{item:NO-rec-primary}
\item Prove that $\ble$ is \emph{antisymmetric}\index{relation!antisymmetric}: if $a\ble b$ and $b\ble a$, then $a=b$.
\item For $x,y$ defined by cuts such that $x^L<y$ for all $L$ and $x<y^R$ for all $R$, and assuming inductively that $f(x^L)\blt f(y)$ for all $L$, $f(x)\blt f(y^R)$ for all $R$, and also that $f(x^L)\blt f(x^R)$ and $f(y^L)\blt f(y^R)$ for all $L$ and $R$, we must prove $f(x)\ble f(y)$.
\item For $x,y$ defined by cuts and an $L_0$ such that $x\le y^{L_0}$, and assuming inductively that $f(x)\ble f(y^{L_0})$, and also that $f(x^L)\blt f(x^R)$ and $f(y^L)\blt f(y^R)$ for all $L$ and $R$, we must prove $f(x)\blt f(y)$.
\item For $x,y$ defined by cuts and an $R_0$ such that $x^{R_0}\le y$, and assuming inductively that $f(x^{R_0})\ble f(y)$, and also that $f(x^L)\blt f(x^R)$ and $f(y^L)\blt f(y^R)$ for all $L$ and $R$, we must prove $f(x)\blt f(y)$.\label{item:NO-rec-last}
\end{enumerate}
The last three clauses can be more concisely described by saying we must prove that $f$ (as defined in the first clause) takes $\le$ to $\ble$ and $<$ to $\blt$.
We will refer to these properties by saying that \emph{$f$ preserves inequalities}.
Moreover, in proving that $f$ preserves inequalities, we may assume the particular instance of $\le$ or $<$ to be obtained from one of its constructors, and we may also use inductive hypotheses that $f$ preserves all inequalities appearing in the input to that constructor.

If we succeed at~\ref{item:NO-rec-primary}--\ref{item:NO-rec-last} above, then we obtain $f:\NO\to A$, which computes on cuts as specified by~\ref{item:NO-rec-primary}, and which preserves all inequalities:
%
\begin{narrowmultline*}
  \fall{x,y:\NO}\Big((x\le y) \to (f(x)\ble f(y))\Big) \land
  \narrowbreak
  \Big((x< y) \to (f(x)\blt f(y))\Big).
\end{narrowmultline*}
%
Like $(\RC,\closesym)$-recursion for the Cauchy reals, this recursion principle is essential for defining functions on $\NO$, since we cannot first define a function on ``pre-surreals'' and only later prove that it respects the notion of equality.

\begin{eg}
  Let us define the \emph{negation} function $\NO\to\NO$.
  We apply the joint recursion principle with $A\defeq\NO$, with $(x\ble y)\defeq (y\le x)$, and $(x\blt y)\defeq (y< x)$.
  Clearly this $\ble$ is antisymmetric.

  For the main clause in the definition, we assume $x$ defined by a cut, with $-x^L$ and $-x^R$ defined such that $-x^L \blt -x^R$ for all $L$ and $R$.
  By definition, this means $-x^R< -x^L$ for all $L$ and $R$, so we can define $-x$ by the cut $\surr{-x^R}{-x^L}$.
  This notation, which follows Conway, refers to the cut whose left options are indexed by the type $\RR$ indexing the right options of $x$, and whose right options are indexed by the type $\LL$ indexing the left options of $x$, with the corresponding families $\RR\to\NO$ and $\LL\to\NO$ defined by composing those for $x$ with negation.

  We now have to verify that $f$ preserves inequalities.
  \begin{itemize}
  \item For $x\le y$, we may assume $x^L<y$ for all $L$ and $x < y^R$ for all $R$, and show $-y\le -x$.
    But inductively, we may assume $-y <-x^L$ and $-y^R<-x$, which gives the desired result, by definition of $-y$, $-x$, and the constructor of $\le$.
  \item For $x<y$, in the first case when it arises from some $x\le y^{L_0}$, we may inductively assume $-y^{L_0} \le -x$, in which case $-y<-x$ follows by the constructor of $<$.
  \item Similarly, if $x<y$ arises from $x^{R_0}\le y$, the inductive hypothesis is $-y \le -x^R$, yielding $-y<-x$ again.
  \end{itemize}
\end{eg}

To do much more than this, however, we will need to characterize the relations $\le$ and $<$ more explicitly, as we did for the Cauchy reals in \cref{thm:RC-sim-characterization}.
Also as there, we will have to simultaneously prove a couple of essential properties of these relations, in order for the induction to go through.

\begin{thm}\label{defn:No-codes}
  There are relations $\mathord\preceq:\NO\to\NO\to\prop$ and $\mathord\prec:\NO\to\NO\to\prop$ such that if $x$ and $y$ are surreals defined by cuts, then
  \begin{align*}
    (x\preceq y) &\defeq
    \big(\fall{L} x^L\prec y\big) \land \big(\fall{R} x\prec y^R\big)\\
    (x\prec y) &\defeq
    \big(\exis{L} x\preceq y^L\big) \lor \big(\exis{R} x^R \preceq y\big).
  \end{align*}
  Moreover, we have
  \begin{equation}\label{eq:NO-codes-unstrict}
    (x\prec y) \to (x\preceq y)
  \end{equation}
  and all the reasonable transitivity properties making $\prec$ and $\preceq$ into a ``bimodule''\index{bimodule} over $\le$ and $<$:
  \begin{equation}\label{eq:NO-codes-transitivity}
    \begin{array}{c@{\hspace{1cm}}c}
      (x \le y) \to (y\preceq z) \to (x\preceq z) &
      (x \preceq y) \to (y\le z) \to (x\preceq z) \\
      (x \le y) \to (y\prec z) \to (x\prec z) &
      (x \preceq y) \to (y< z) \to (x\prec z) \\
      (x < y) \to (y\preceq z) \to (x\prec z) &
      (x \prec y) \to (y\le z) \to (x\prec z).
  \end{array}
  \end{equation}
\end{thm}

\begin{proof}
  We define $\preceq$ and $\prec$ by double $(\NO,\le,<)$-induction on $x,y$.
  The first induction is a simple recursion, whose codomain is the subset $A$ of $(\NO\to\prop)\times (\NO\to\prop)$ consisting of pairs of predicates of which one implies the other and which satisfy ``transitivity on the right'', i.e.~\eqref{eq:NO-codes-unstrict} and the right column of~\eqref{eq:NO-codes-transitivity} with $(x\preceq \blank)$ and $(x\prec \blank)$ replaced by the two given predicates.
  As in the proof of \cref{defn:RC-approx}, we regard these predicates as half of binary relations, writing them as $y\mapsto (\hle y)$ and $y\mapsto (\hlt y)$, with $\hlname$ denoting the pair of relations.
  % The precise definition of $A$ is
  % \begin{align*}
  %   A\defeq \bigg\{ \hlname : (\NO\to\prop)\times (\NO\to\prop) \;\bigg|\;\\
  %   \begin{split}
  %     \fall{y,z:\NO}
  %     &\Big( (\hle y) \to (y\le z) \to (\hle z) \Big)\\
  %     \land\; &\Big( (\hle y) \to (y< z) \to (\hlt z) \Big)\\
  %     \land\; &\Big( (\hlt y) \to (y\le z) \to (\hlt z) \Big)\\
  %     \land\; &\Big( (\hlt y) \to (y< z) \to (\hlt z) \Big) \bigg\}
  %   \end{split}
  % \end{align*}
  We equip $A$ with the following two relations:
  \begin{align*}
    (\hlname \ble \hlbname) &\defeq
    \fall{y:\NO} \Big( (\hleb y) \to (\hle y) \Big) \land
    \Big( (\hltb y) \to (\hlt y) \Big),\\
    (\hlname \blt \hlbname) &\defeq
    \fall{y:\NO} \Big( (\hleb y) \to (\hlt y) \Big).
    %\land \Big( (\hltb y) \to (\hlt y) \Big)
  \end{align*}
  Note that $\ble$ is antisymmetric, since if $\hlname \ble \hlbname$ and $\hlbname \ble \hlname$, then $(\hleb y) \Leftrightarrow (\hle y)$ and $(\hltb y) \Leftrightarrow (\hlt y)$ for all $y$, hence $\hlname=\hlbname$ by univalence for mere propositions and function extensionality.
  Moreover, to say that a function $\NO\to A$ preserves inequalities is exactly to say that, when regarded as a pair of binary relations on $\NO$, it satisfies ``transitivity on the left'' (the left column of~\eqref{eq:NO-codes-transitivity}).

  Now for the primary clause of the recursion, we assume given $x$ defined by a cut, and relations $(x^L \prec \blank)$, $(x^R \prec \blank)$, $(x^L \preceq \blank)$, and $(x^R \preceq \blank)$ for all $L$ and $R$, of which the strict ones imply the non-strict ones, which satisfy transitivity on the right, and such that
  \begin{equation}\label{eq:NO-prec-outer-IH}
    \fall{L,R}{y:\NO}\Big( (x^R\preceq y) \to (x^L \prec y) \Big).
    % \land\Big( (x^R \prec y) \to (x^L \prec y) \Big)
  \end{equation}
  We now have to define $(x\prec y)$ and $(x\preceq y)$ for all $y$.
  Here in contrast to \cref{defn:RC-approx}, rather than a nested recursion, we use a nested induction, in order to be able to inductively use transitivity on the left with respect to the inequalities $x^L<x$ and $x<x^R$.
  Define $A':\NO\to\type$ by taking $A'(y)$ to be the subset $A'$ of $\prop\times\prop$ consisting of two mere propositions, denoted $\tle y$ and $\tlt y$ (with $\tlname:A'(y)$), such that
  \begin{gather}
    (\tlt y) \to (\tle y)\\
    \fall{L} (\tle y)\to (x^L\prec y) \label{eq:NO-prec-IHL}\\
    \fall{R} (x^R \preceq y) \to (\tlt y) \label{eq:NO-prec-IHR}.
  \end{gather}
  Using notation analogous to $\ble$ and $\blt$, we equip $A'$ with the two relations defined for $\tlname:A'(y)$ and $\tlbname:A'(z)$ by
  \begin{align*}
    (\tlname \bble \tlbname) &\defeq
    \Big((\tle y) \to (\tleb z)\Big) \land \Big((\tlt y) \to (\tltb z)\Big)\\
    (\tlname \bblt \tlbname) &\defeq
    \Big((\tle y) \to (\tltb z)\Big). % \land \Big(\tlt \to \tltb\Big).
  \end{align*}
  % (These are the type families $B$ and $C$ in the general induction principle.)
  Again, $\bble$ is evidently antisymmetric in the appropriate sense.
  Moreover, a function $\prd{y:\NO} A'(y)$ which preserves inequalities is precisely a pair of predicates of which one implies the other, which satisfy transitivity on the right, and transitivity on the left with respect to the inequalities $x^L<x$ and $x<x^R$.
  Thus, this inner induction will provide what we need to complete the primary clause of the outer recursion.

  For the primary clause of the inner induction, we assume also given $y$ defined by a cut, and properties $(x\prec y^L)$, $(x\prec y^R)$, $(x\preceq y^L)$, and $(x\preceq y^R)$ for all $L$ and $R$, with the strict ones implying the non-strict ones, transitivity on the left with respect to $x^L<x$ and $x<x^R$, and on the right with respect to $y^L<y^R$.
  % \begin{equation}
  %   \fall{L,R}\Big((x \preceq y^L) \to (x \prec y^R)\Big) % \land \Big((x \prec y^L) \to (x\prec y^R)\Big).
  %   \label{eq:NO-prec-inner-IH}
  % \end{equation}
  We can now give the definitions specified in the theorem statement:
  \begin{align}
    (x\preceq y) &\defeq
    (\fall{L} x^L\prec y) \land (\fall{R} x\prec y^R), \label{eq:NO-preceq-def}\\
    (x\prec y) &\defeq
    (\exis{L} x\preceq y^L) \lor (\exis{R} x^R \preceq y).\label{eq:NO-prec-def}
  \end{align}
  For this to define an element of $A'(y)$, we must show first that $(x\prec y) \to (x\preceq y)$.
  The assumption $x\prec y$ has two cases.
  On one hand, if there is $L_0$ with $x\preceq y^{L_0}$, then by transitivity on the right with respect to $y^{L_0}<y^R$, we have $x\prec y^R$ for all $R$.
  Moreover, by transitivity on the left with respect to $x^L<x$, we have $x^L \prec y^{L_0}$ for any $L$, hence $x^L\prec y$ by transitivity on the right.
  Thus, $x\preceq y$.

  On the other hand, if there is $R_0$ with $x^{R_0}\preceq y$, then by~\eqref{eq:NO-prec-outer-IH}, we have $x^L \prec y$ for all $L$.
  And by transitivity on the left and right with respect to $x<x^{R_0}$ and $y<y^R$, we have $x\prec y^R$ for any $R$.
  Thus, $x\preceq y$.

  We also need to show that these definitions are transitive on the left with respect to $x^L<x$ and $x<x^R$.
  But if $x\preceq y$, then $x^L\prec y$ for all $L$ by definition; while if $x^R\preceq y$, then $x\prec y$ also by definition.

  Thus,~\eqref{eq:NO-preceq-def} and~\eqref{eq:NO-prec-def} do define an element of $A'(y)$.
  We now have to verify that this definition preserves inequalities, as a dependent function into $A'$, i.e.\ that these relations are transitive on the right.
  Remember that in each case, we may assume inductively that they are transitive on the right with respect to all inequalities arising in the inequality constructor.
  \begin{itemize}
  \item Suppose $x\preceq y$ and $y\le z$, the latter arising from $y^L<z$ and $y<z^R$ for all $L$ and $R$.
    Then the inductive hypothesis (of the inner recursion) applied to $y<z^R$ yields $x\prec z^R$ for any $R$.
    Moreover, by definition $x\preceq y$ implies that $x^L \prec y$ for any $L$, so by the inductive hypothesis of the outer recursion we have $x^L \prec z$.
    Thus, $x\preceq z$.
  \item Suppose $x\preceq y$ and $y<z$.
    First, suppose $y<z$ arises from $y\le z^{L_0}$.
    Then the inner inductive hypothesis applied to $y\le z^{L_0}$ yields $x \preceq z^{L_0}$, hence $x\prec z$.

    Second, suppose $y<z$ arises from $y^{R_0}\le z$.
    Then by definition, $x\preceq y$ implies $x\prec y^{R_0}$, and then the inner inductive hypothesis for $y^{R_0}\le z$ yields $x\prec z$.
  \item Suppose $x\prec y$ and $y\le z$, the latter arising from $y^L<z$ and $y<z^R$ for all $L$ and $R$.
    By definition, $x\prec y$ implies there merely exists $R_0$ with $x^{R_0}\preceq y$ or $L_0$ with $x\preceq y^{L_0}$.
    If $x^{R_0}\preceq y$, then the outer inductive hypothesis yields $x^{R_0}\preceq z$, hence $x\prec z$.
    If $x\preceq y^{L_0}$, then the inner inductive hypothesis for $y^{L_0}<z$ (which holds by the constructor of $y\le z$) yields $x\prec z$.
  % \item Suppose $x\prec y$ and $y<z$.
  %   First, suppose $y<z$ arises from $y\le z^{L_0}$.
  %   Then the inner inductive hypothesis for $y\le z^{L_0}$ yields $x\prec z^{L_0}$, hence $x\preceq z^{L_0}$; thus $x\prec z$.

  %   Second, suppose $y<z$ arises from $y^{R_0}\le z$.
  %   Then by definition, $x\prec y$ implies there merely exists $R_1$ with $x^{R_1}\preceq y$ or $L_1$ with $x\preceq y^{L_1}$.
  %   If $x^{R_1}\preceq y$, then the outer inductive hypothesis implies $x^{R_1}\prec z$, hence $x^{R_1}\preceq z$, and thus $x\prec z$.
  %   And if $x\preceq y^{L_1}$, then the inner inductive hypothesis applied to $y^{L_1}<y^{R_0}$ (which comes from $y$ being defined as a cut) and $y^{R_0}\le z$ yields $x\prec z$.
  \end{itemize}
  This completes the inner induction.
  Thus, for any $x$ defined by a cut, we have $(x\prec \blank)$ and $(x\preceq \blank)$ defined by~\eqref{eq:NO-preceq-def} and~\eqref{eq:NO-prec-def}, and transitive on the right.

  To complete the outer recursion, we need to verify these definitions are transitive on the left.
  After a $\NO$-induction on $z$, we end up with three cases that are essentially identical to those just described above for transitivity on the right.
  Hence, we omit them.
\end{proof}

\begin{thm}\label{thm:NO-encode-decode}
  For any $x,y:\NO$ we have $(x<y)=(x\prec y)$ and $(x\le y)=(x\preceq y)$.
\end{thm}
\begin{proof}
  From left to right, we use $(\NO,\le,<)$-induction where $A(x)\defeq\unit$, with $\preceq$ and $\prec$ supplying the relations $\ble$ and $\blt$.
  In all the constructor cases, $x$ and $y$ are defined by cuts, so the definitions of $\preceq$ and $\prec$ evaluate, and the inductive hypotheses apply.

  From right to left, we use $\NO$-induction to assume that $x$ and $y$ are defined by cuts.
  But now the definitions of $\preceq$ and $\prec$, and the inductive hypotheses, supply exactly the data required for the relevant constructors of $\le$ and $<$.
  % From right to left, we first prove by $\NO$-induction on $x$ that for any $y:\NO$ we have $(x\prec y) \to (x<y)$ and $(x\preceq y) \to (x\le y)$.
  % Thus, we assume this to be true for all $x^L$ and $x^R$ in a cut, and show it for the resulting $x:\NO$.
  % Next, we prove by $\NO$-induction on $y$ that $(x\prec y) \to (x<y)$ and $(x\preceq y) \to (x\le y)$, hence we assume it to be true for all $y^L$ and $y^R$ in a cut, and show it for the resulting $y:\NO$.
  % Now since $x$ and $y$ are both defined by cuts, $x\preceq y$ means that $x^L\prec y$ and $x\prec y^R$ for all $L$ and $R$.
  % By the inductive hypotheses, this gives $x^L<y$ and $x<y^R$, hence $x\le y$ by the constructor of $\le$.
  % Similarly, $x\prec y$ yields merely an $R_0$ with $x^{R_0}\preceq y$ or an $L_0$ with $x\preceq y^{L_0}$.
  % Hence merely $x^{R_0}\le y$ or $x\le y^{L_0}$ by the inductive hypothesis, so $x<y$ by a constructor.
\end{proof}

\begin{cor}\label{thm:NO-unstrict-transitive}
  The relations $\le$ and $<$ on $\NO$ satisfy
  \[ \fall{x,y:\NO} (x<y) \to (x\le y) \]
  and are transitive:
  \index{transitivity!of . for surreals@of $<$ for surreals}
  \index{transitivity!of . for surreals@of $\leq$ for surreals}
  \begin{gather*}
    (x\le y) \to (y\le z) \to (x\le z)\\
    (x\le y) \to (y< z) \to (x< z)\\
    (x< y) \to (y\le z) \to (x< z).
  \end{gather*}
\end{cor}

As with the Cauchy reals, the joint $(\NO,\le,<)$-recursion principle remains essential when defining all operations on $\NO$.

\begin{eg}\label{eg:surreal-addition}
\index{addition!of surreal numbers}%
We define $\mathord+:\NO\to\NO\to\NO$ by recursion on the first argument, followed by induction on the second argument.
For the outer recursion, we take the codomain to be the subset of $\NO\to\NO$ consisting of functions $g$ such that $(x<y) \to (g(x)<g(y))$ and $(x\le y) \to (g(x)\le g(y))$ for all $x,y$.
For such $g,h$ we define $(g\ble h)\defeq \fall{x:\NO} g(x)\le h(x)$ and $(g\blt h)\defeq \fall{x:\NO} g(x)< h(x)$.
Clearly $\ble$ is antisymmetric.

For the primary clause of the recursion, we suppose $x$ defined by a cut, that the functions $(x^L+\blank)$ and $(x^R+\blank)$ are defined, preserve inequalities, and satisfy $x^L+y<x^R+y$, and we define $(x+\blank)$.
As in \cref{defn:No-codes}, rather than an inner recursion, we use an inner induction into the family $A:\NO\to\type$, where $A(y)$ is the subset of those $z:\NO$ such that each $x^L + y < z$ and each $x^R + y > z$.
We equip $A$ with the relations $\le$ and $<$ induced from $\NO$, so that antisymmetry is obvious.
For the primary clause of the inner recursion, we suppose also $y$ defined by a cut, with each $x+y^L$ and $x+y^R$ defined and satisfying $x^L+y^L < x+y^L$, $x^L+y^R < x+y^R$, $x+y^L < x^R + y^L$, and $x+y^R < x^R+y^R$ (these come from the additional conditions imposed on elements of $A(y)$), and also $x+y^L < x+y^R$ (since the elements $x+y^L$ and $x+y^R$ of $A(y)$ form a dependent cut).
Now we give Conway's definition:
\[ x+y \defeq \surr{x^L+y, x+y^L}{x^R+y,x+y^R}. \]
In other words, the left options of $x+y$ are all numbers of the form $x^L+y$ for some left option $x^L$, or $x+y^L$ for some left option $y^L$.
We must show that each of these left options is less than each of these right options:
\begin{itemize}
\item $x^L+y < x^R+y$ by the outer inductive hypothesis.
\item $x^L+y < x^L + y^R < x + y^R$, the first since $(x^L+\blank)$ preserves inequalities, and the second since $x+y^R : A(y^R)$.
\item $x+y^L < x^R+ y^L < x^R + y$, the first since $x+y^L : A(y^L)$ and the second since $(x^R+\blank)$ preserves inequalities.
\item $x+y^L < x+y^R$ by the inner inductive hypothesis (specifically, the fact that we have a dependent cut).
\end{itemize}
We also have to show that $x+y$ thusly defined lies in $A(y)$, i.e.\ that $x^L + y < x+y$ and $x+y < x^R + y$; but this is true by \cref{thm:NO-refl-opt}\ref{item:NO-lt-opt}.

Next we have to verify that the definition of $(x+\blank)$ preserves inequality:
\begin{itemize}
\item If $y\le z$ arises from knowing that $y^L<z$ and $y<z^R$ for all $L$ and $R$, then the inner inductive hypothesis gives $x+y^L<x+z$ and $x+y < x+z^R$, while the outer inductive hypotheses give $x^L+y \le x^L+z$ and $x^R+ y \le x^R+z$.
  Moreover, since $x^R+y$ is by definition a right option of $x+y$, we have $x+y < x^R+y$.
  Similarly, we find that $x^L+z$ is a left option of $x+z$, so that $x^L+z < x+z$.
  Thus, using transitivity, we have $x^L+y < x+z$ and $x+y < x^R+z$; so we may conclude $x+y \le x+z$ by the constructor of $\le$.
\item If $y<z$ arises from an $L_0$ with $y\le z^{L_0}$, then inductively $x+y \le x+z^{L_0}$, hence $x+y<x+z$ since $x+z^{L_0}$ is a right option of $x+z$.
\item Similarly, if $y<z$ arises from $y^{R_0}\le z$, then $x+y<x+z$ since $x+y^{R_0}\le x+z$.
\end{itemize}
This completes the inner induction.
For the outer recursion, we have to verify that $+$ preserves inequality on the left as well.
After an $\NO$-induction, this proceeds in exactly the same way.
\end{eg}

\index{acceptance|(}%
\index{mathematics!formalized}%
In the Appendix to Part Zero of~\cite{conway:onag}, Conway discusses how the surreal numbers may be formalized in ZFC set theory: by iterating along the ordinals and passing to sets of representatives of lowest rank for each equivalence class, or by representing numbers with ``sign-expansions''.
He then remarks that
\begin{quote}\footnotesize
  The curiously complicated nature of these constructions tells us more about the nature of formalizations within ZF than about our system of numbers\dots
\end{quote}
and goes on to advocate for a general theory of ``permissible kinds of construction'' which should include
\begin{enumerate}\footnotesize
\item Objects may be created from earlier objects in any reasonably constructive fashion.\label{item:conway1}
\item Equality among the created objects can be any desired equivalence relation.\label{item:conway2}
\end{enumerate}
\noindent
Condition~\ref{item:conway1} can be naturally read as justifying general principles of \emph{inductive definition}, such as those presented in \cref{sec:strictly-positive,sec:generalizations}.
In particular, the condition of strict positivity for constructors can be regarded as a formalization of what it means to be ``reasonably constructive''.
Condition~\ref{item:conway2} then suggests we should extend this to \emph{higher} inductive definitions of all sorts, in which we can impose path constructors making objects equal in any reasonable way.
For instance, in the next paragraph Conway says:
\begin{quote}\footnotesize
  \dots we could also, for instance, freely create a new object $(x,y)$ and call it the ordered pair of $x$ and $y$.
  We could also create an ordered pair $[x,y]$ different from $(x,y)$ but co-existing with it\dots
  If instead we wanted to make $(x,y)$ into an unordered pair, we could define equality by means of the equivalence relation $(x,y)=(z,t)$ if and only if $x=z,y=t$ \emph{or} $x=t,y=z$.
\end{quote}
The freedom to introduce new objects with new names, generated by certain forms of constructors, is precisely what we have in the theory of inductive definitions.
Just as with our two copies of the natural numbers $\nat$ and $\nat'$ in \cref{sec:appetizer-univalence}, if we wrote down an identical definition to the cartesian product type $A\times B$, we would obtain a distinct product type $A\times' B$ whose canonical elements we could freely write as $[x,y]$.
And we could make one of these a type of unordered pairs by adding a suitable path constructor. % (and perhaps 0-truncating).

To be sure, Conway's point was not to complain about ZF in particular, but to argue against all foundational theories at once:
\begin{quote}\footnotesize
  \dots this proposal is not of any particular theory as an alternative to ZF\dots{}
  What is proposed is instead that we give ourselves the freedom to create arbitrary mathematical theories of these kinds, but prove a metatheorem which ensures once and for all that any such theory could be formalized in terms of any of the standard foundational theories.
\end{quote}
One might respond that, in fact, univalent foundations is not one of the ``standard foundational theories'' which Conway had in mind, but rather the \emph{metatheory} in which we may express our ability to create new theories, and about which we may prove Conway's metatheorem.
For instance, the surreal numbers are one of the ``mathematical theories'' Conway has in mind, and we have seen that they can be constructed and justified inside univalent foundations.
Similarly, Conway remarked earlier that
\begin{quote}\footnotesize
  \dots set theory would be such a theory, sets being constructed from earlier ones by processes corresponding to the usual axioms, and the equality relation being that of having the same members.
\end{quote}
This description closely matches the higher-inductive construction of the cumulative hierarchy of set theory in \cref{sec:cumulative-hierarchy}.
Conway's metatheorem would then correspond to the fact we have referred to several times that we can construct a model of univalent foundations inside ZFC (which is outside the scope of this book).

However, univalent foundations is so rich and powerful in its own right that it would be foolish to relegate it to only a metatheory in which to construct set-like theories.
We have seen that even at the level of sets (0-types), the higher inductive types in univalent foundations yield direct constructions of objects by their universal properties (\cref{sec:free-algebras}), such as a constructive theory of Cauchy completion (\cref{sec:cauchy-reals}).
But most importantly, the potential to model homotopy theory and category theory directly in the foundational system (\cref{cha:homotopy,cha:category-theory}) gives univalent foundations an advantage which no set-theoretic foundation can match.
\index{acceptance|)}%

\index{surreal numbers|)}%

\sectionNotes

Defining algebraic operations on Dedekind reals, especially multiplication, is both somewhat tricky and tedious.
There are several ways to get arithmetic going: each has its own advantages, but they all seem to require some technical work.
For instance, Richman~\cite{Richman:reals} defines multiplication on the Dedekind reals first on the positive cuts and then extends it algebraically to all Dedekind cuts, while Conway~\cite{conway:onag} has observed that the definition of multiplication for surreal numbers works well for Dedekind reals.

Our treatment of the Dedekind reals borrows many ideas from~\cite{BauerTaylor09} where the Dedekind reals are constructed in the context of Abstract Stone Duality.
\index{Abstract Stone Duality}%
This is a (restricted) form of simply typed $\lambda$-calculus with a distinguished object $\Sigma$ which classifies open sets, and by duality also the closed ones. In~\cite{BauerTaylor09} you can also find detailed proofs of the basic properties of arithmetical operations.

The fact that $\RC$ is the least Cauchy complete archimedean ordered field, as was proved in \cref{RC-initial-Cauchy-complete}, indicates that our Cauchy reals probably coincide with the Escard{\'o}-Simpson reals~\cite{EscardoSimpson:01}.
\index{real numbers!Escardo-Simpson@Escard\'o-Simpson}%
It would be interesting to check\index{open!problem} whether this is really the case. The notion of Escard{\'o}-Simpson reals, or more precisely the corresponding closed interval, is interesting because it can be stated in any category with finite products.

In constructive set theory augmented by the ``regular extension axiom'', one may also try to define Cauchy completion by closing under limits of Cauchy sequences with a transfinite iteration.
It would also be interesting to check whether this construction agrees with ours.

It is constructive folklore that coincidence of Cauchy and Dedekind reals requires dependent choice but it is less well known that countable choice suffices. Recall that \define{dependent choice}
\indexdef{axiom!of choice!dependent}%
\index{axiom!of choice!countable}%
\index{total!relation}%
states that for a total relation $R$ on $A$, by which we mean $\fall{x : A} \exis{y : A} R(x,y)$, and for any $a : A$ there merely exists $f : \N \to A$ such that $f(0) = a$ and $R(f(n), f(n+1))$ for all $n : \N$. Our \cref{when-reals-coincide} uses the typical trick for converting an application of dependent choice to one using countable choice. Namely, we use countable choice once to make in advance all the choices that could come up, and then use the choice function to avoid the dependent choices.

The intricate relationship between various notions of compactness in a constructive
setting is discussed in \cite{bridges2002compactness}. Palmgren~\cite{Palmgren:FT} has a
good comparison between pointwise analysis and
pointfree topology.

The surreal numbers were defined by~\cite{conway:onag}, using a sort of inductive definition but without justifying it explicitly in terms of any foundational system.
For this reason, some later authors have tended to use sign-expansions or other more explicit presentations which can be coded more obviously into set theory.
The idea of representing them in type theory was first considered by Hancock, while
Setzer and Forsberg~\cite{forsbergfinite} noted that the surreals and their inequality relations $<$ and $\le$ naturally form an inductive-inductive definition.
The \emph{higher} inductive-inductive version presented here, which builds in the correct notion of equality for surreals, is new.


\sectionExercises

\begin{ex}\label{ex:alt-dedekind-reals}
 Give an alternative definition of the Dedekind reals by first defining the square and then use \cref{mult-from-square}.
 Check that one obtains a commutative ring.
\end{ex}

\begin{ex} \label{ex:RD-extended-reals}
  %
  Suppose we remove the boundedness condition in \cref{defn:dedekind-reals}.
  Then we obtain the \define{extended reals}
  \indexdef{real numbers!extended}%
  \indexdef{extended real numbers}%
  which contain $-\infty \defeq
  (\emptyt, \Q)$ and $\infty \defeq (\Q, \emptyt)$. Which definitions of arithmetical
  operations on cuts still make sense for extended reals? What algebraic structure do we
  get?
\end{ex}

\begin{ex} \label{ex:RD-lower-cuts}
  %
  By considering one-sided cuts we obtain \define{lower} and \define{upper} Dedekind reals,
  \indexdef{real numbers!Dedekind!upper}%
  \indexdef{real numbers!Dedekind!lower}%
  \indexdef{lower Dedekind reals}%
  \indexdef{upper Dedekind reals}%
  \index{cut!Dedekind}%
  respectively. For example, a lower real is given by a predicate $L : \Q \to \Omega$
  which is
  %
  \begin{enumerate}
  \item \emph{inhabited:} $\exis{q : \Q} L(q)$ and
  \item \emph{rounded:} $L(q) = \exis{r : \Q} q < r \land L(r)$.
    \index{rounded!Dedekind cut}
  \end{enumerate}
  %
  (We could also require $\exis{r : \Q} \lnot L(r)$ to exclude the cut $\infty \defeq
  \Q$.) Which arithmetical operations can you define on the lower reals? In particular,
  what happens with the additive inverse?
\end{ex}

\begin{ex} \label{ex:RD-interval-arithmetic}
  %
  \index{interval!arithmetic}%
  Suppose we remove the locatedness condition in \cref{defn:dedekind-reals}.
  Then we obtain the \define{interval domain}
  \indexdef{interval!domain}%
  $\mathbb{I}$ because cuts are allowed
  to have ``gaps'', which are just intervals. Define the partial order $\sqsubseteq$ on
  $\mathbb{I}$ by
  %
  \begin{narrowmultline*}
    ((L, U) \sqsubseteq (L', U'))
    \defeq \narrowbreak
    (\fall{q : \Q} L(q) \Rightarrow L'(q)) \land
    (\fall{q : \Q} U(q) \Rightarrow U'(q)).
  \end{narrowmultline*}
  %
  What are the maximal elements of $\mathbb{I}$ with respect to $\mathbb{I}$? Define the
  ``endpoint'' operations which assign to an element of the interval domain its lower and
  upper endpoints. Are the endpoints reals, lower reals, or upper reals (see
  \cref{ex:RD-lower-cuts})? Which definitions of arithmetical operations on cuts still
  make sense for the interval domain?
\end{ex}

\begin{ex} \label{ex:RD-lt-vs-le}
  Show that, for all $x, y : \RD$,
  %
  \begin{equation*}
    \lnot (x < y) \Rightarrow y \leq x
  \end{equation*}
  %
  and
  %
  \begin{equation*}
    \eqv{(x \leq y)}{\Parens{\prd{\epsilon : \Qp} x < y + \epsilon}}.
  \end{equation*}
  %
  Does $\lnot (x \leq y)$ imply $y < x$?
\end{ex}

\begin{ex} \label{ex:reals-non-constant-into-Z}
  \mbox{}
  %
  \begin{enumerate}
  \item
    Assuming excluded middle, construct a non-constant map $\RD \to \Z$.
  \item
    Suppose $f : \RD \to \Z$ is a map such that $f(0) = 0$ and $f(x) \neq 0$ for all $x >
    0$. Derive from this the limited principle of omniscience~\eqref{eq:lpo}.
\index{limited principle of omniscience}%
  \end{enumerate}
\end{ex}

\begin{ex} \label{ex:traditional-archimedean}
  \index{ordered field!archimedean}%
  Show that in an ordered field $F$, density of $\Q$ and the traditional archimedean axiom
  are equivalent:
  %
  \begin{equation*}
    (\fall{x, y : F} x < y \Rightarrow \exis{q : \Q} x < q < y)
    \Leftrightarrow
    (\fall{x : F} \exis{k : \Z} x < k).
  \end{equation*}
\end{ex}

\begin{ex} \label{RC-Lipschitz-on-interval} Suppose $a, b : \Q$ and $f : \setof{ q : \Q |
    a \leq q \leq b } \to \RC$ is Lipschitz with constant~$L$. Show that there exists a unique
  extension $\bar{f} : [a,b] \to \RC$ of $f$ which is Lipschitz with
  constant~$L$. Hint: rather than redoing \cref{RC-extend-Q-Lipschitz} for closed
  intervals, observe that there is a retraction $r : \RC \to [-n,n]$ and apply
  \cref{RC-extend-Q-Lipschitz} to $f \circ r$.
\end{ex}

\begin{ex} \label{ex:metric-completion}
  \index{completion!of a metric space}%
  Generalize the construction of $\RC$ to construct the Cauchy completion of any metric space. First, think about which notion of real numbers is most natural as the codomain for the distance\index{distance} function of a metric space. Does it matter? Next, work out the details of two constructions:
  %
  \begin{enumerate}
  \item Follow the construction of Cauchy reals to define the completion of a metric space as an inductive-inductive type closed under limits of Cauchy sequences.\index{Cauchy!sequence}
  \item Use the following construction due to Lawvere~\cite{lawvere:metric-spaces}\index{Lawvere} and Richman~\cite{Richman00thefundamental}, where the completion of a metric space $(M, d)$ is given as the type of \define{locations}.
    \indexdef{location}%
    A location is a function $f : M \to \R$ such that
    %
    \begin{enumerate}
    \item $f(x) \geq |f(y) - d(x,y)|$ for all $x, y : M$, and
    \item $\inf_{x \in M} f(x) = 0$, by which we mean $\fall{\epsilon : \Qp} \exis{x : M} |f(x)| < \epsilon$ and $\fall{x : M} f(x) \geq 0$.
    \end{enumerate}
    %
    The idea is that $f$ looks like it is measuring the distance from a point.
  \end{enumerate}
  %
  \index{universal!property!of metric completion}%
  Finally, prove the following universal property of metric completions: a locally uniformly continuous map from a metric space to a Cauchy complete metric space extends uniquely to a locally uniformly continuous map on the completion. (We say that a map is \define{locally uniformly continuous}
  \indexdef{function!locally uniformly continuous}%
  \indexdef{locally uniformly continuous map}%
  if it is uniformly continuous on open balls.)
\end{ex}

\index{metric space|)}%

\begin{ex} \label{ex:reals-apart-neq-MP}
  \define{Markov's principle}
  \indexdef{axiom!Markov's principle}%
  \indexdef{Markov's principle}%
  says that for all $f : \nat \to \bool$,
  %
  \begin{equation*}
    (\lnot \lnot \exis{n : \nat} f(n) = \btrue)
    \Rightarrow
    \exis{n : \nat} f(n) = \btrue.
  \end{equation*}
  %
  This is a particular instance of the law of double negation~\eqref{eq:ldn}. Show that
  $\fall{x, y: \RD} x \neq y \Rightarrow x \apart y$ implies Markov's principle. Does the
  converse hold as well?
\end{ex}

\begin{ex} \label{ex:reals-apart-zero-divisors}
  \index{apartness}%
  Verify that the following ``no zero divisors'' property holds for the real numbers:
  $x y \apart 0 \Leftrightarrow x \apart 0 \land y \apart 0$.
\end{ex}

\begin{ex} \label{ex:finite-cover-lebesgue-number}
  %
  Suppose $(q_1, r_1), \ldots, (q_n, r_n)$ pointwise cover $(a, b)$. Then there is
  $\epsilon : \Qp$ such that whenever $a < x < y < b$ and $|x - y| < \epsilon$
  then there merely exists $i$ such that $q_i < x < r_i$ and $q_i < y < r_i$. Such an
  $\epsilon$ is called a \define{Lebesgue number}
  \indexdef{Lebesgue number}%
  for the given cover.
\end{ex}

\begin{ex} \label{ex:mean-value-theorem}
  %
  Prove the following approximate version of the intermediate value theorem:
  %
  \begin{quote}
    \emph{
      If $f : [0,1] \to \R$ is uniformly continuous and $f(0) < 0 < f(1)$ then
      for every $\epsilon : \Qp$ there merely exists $x : [0,1]$ such that $|f(x)| <
      \epsilon$.
    }
  \end{quote}
  %
  Hint: do not try to use the bisection method because it leads to the axiom of choice.
  Instead, approximate $f$ with a piecewise linear map. How do you construct a piecewise
  linear map?
\end{ex}

\begin{ex}\label{ex:knuth-surreal-check}
  Check whether everything in~\cite{knuth74:_surreal_number} can be done using the higher
  inductive-inductive surreals of \cref{sec:surreals}.
\end{ex}

\begin{ex}\label{ex:reals-into-surreals}
  Recall the function $\iota_{\RD}:\RD\to\NO$ defined on page~\pageref{reals-into-surreals}.
  \begin{enumerate}
  \item Show that $\iota_{\RD}$ is injective.
  \item There are obvious extensions of $\iota_{\RD}$ to the extended reals (\cref{ex:RD-extended-reals}) and the interval domain (\cref{ex:RD-interval-arithmetic}).
    Are they injective?
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:ord-into-surreals}
  Show that the function $\iota_{\ord}:\ord\to\NO$ defined on page~\pageref{ord-into-surreals} is injective if and only if \LEM{} holds.
\end{ex}

\begin{ex}\label{ex:hiit-plump}
  Define a type $\mathsf{POrd}$ equipped with binary relations $\le$ and $<$ by mimicking the definition of \NO but using only left options.
  \begin{enumerate}
  \item Construct a map $j:\mathsf{POrd} \to \NO$ and show that it is an embedding.
  \item Show that $\mathsf{POrd}$ is an ordinal (in the next higher universe, like \ord) under the relation $<$.
  \item Assuming propositional resizing, show that $\mathsf{POrd}$ is equivalent to the subset
    \[\setof{A:\ord | \mathsf{isPlump}(A)}\]
    of \ord from \cref{ex:plump-ordinals}.
    Conclude that $\iota_{\ord}:\ord\to\NO$ is injective when restricted to plump ordinals.
  \end{enumerate}
  In the absence of propositional resizing, we may still refer to elements of $\mathsf{POrd}$ (or their images in \NO) as \define{plump ordinals}.\index{ordinal!plump}\index{plump!ordinal}
\end{ex}

\begin{ex}\label{ex:pseudo-ordinals}
  Define a surreal number to be a \define{pseudo-ordinal}\index{pseudo-ordinal}\index{ordinal!pseudo-} if it is equal to a cut $\surr{x^L}{}$ with no right options (but its left options may themselves have right options).
  Show that the statement ``every pseudo-ordinal is a plump ordinal'' is equivalent to \LEM{}.
\end{ex}

\begin{ex}\label{ex:double-No-recursion}
  Note that \cref{defn:No-codes} and \cref{eg:surreal-addition} both use a similar pattern to define a function $\NO \to \NO \to B$: an outer \NO-recursion whose codomain is the set of order-preserving functions $\NO\to B$, followed by an inner \NO-induction into a family $A:\NO\to\type$ where $A(y)$ is a subset of $B$ ensuring that the inequalities $x^L<x$ and $x<x^R$ are also preserved.
  Formulate and prove a general principle of ``double \NO-recursion'' that generalizes these proofs.
\end{ex}

\index{real numbers|)}%

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "hott-online"
%%% End: