Gaëtan GilbertENS<EMAIL_ADDRESS>
# Formalising Real Numbers in Homotopy Type Theory

###### Abstract

Cauchy reals can be defined as a quotient of Cauchy sequences of rationals.
The limit of a Cauchy sequence of Cauchy reals is defined through lifting it
to a sequence of Cauchy sequences of rationals.

This lifting requires the axiom of countable choice or excluded middle,
neither of which is available in homotopy type theory. To address this, the
Univalent Foundations Program uses a higher inductive-inductive type to define
the Cauchy reals as the free Cauchy complete metric space generated by the
rationals.

We generalize this construction to define the free Cauchy complete metric
space generated by an arbitrary metric space. This forms a monad in the
category of metric spaces with Lipschitz functions. When applied to the
rationals it defines the Cauchy reals. Finally, we can use Altenkirch and
Danielson (2016)’s partiality monad to define a semi-decision procedure
comparing a real number and a rational number.

The entire construction has been formalized in the Coq proof assistant. It is
available at https://github.com/SkySkimmer/HoTTClasses/tree/CPP2017.

##  1 Introduction

The usual process of defining the set of Cauchy real numbers proceeds in three
stages: first define Cauchy sequences of rationals, then define an equivalence
between Cauchy sequences, and finally quotient Cauchy sequences by the
equivalence. However, proving that the so-defined Cauchy reals are Cauchy
complete, i.e. that Cauchy sequences of Cauchy reals have Cauchy real limits
requires the axiom of countable choice.

Alternatively, the quotient step can be replaced by working with Cauchy
sequences as a setoid: this approach is used e.g. in OConnor07 [2007] which
defines the completion of arbitrary metric spaces. This comes at the cost of
having to make all of abstract algebra be about setoids in order to use its
results for real numbers. Moreover, in the context of homotopy type theory we
would like to be able to use the large amount of results about the homotopic
identity but we can only do so for results about identities between bare
Cauchy sequences. For instance, suppose we wish to use the principle of unique
choice (which is true in homotopy type theory) to construct the unique
$x:\mathbb{R}$ such that $P(x)$. Since there are multiple different Cauchy
sequences representing the same real number, this will in fact only be
possible if $P$ does not respect the setoid equivalence, i.e. it should be
considered a property on Cauchy sequences rather than a property on real
numbers.

The Higher Inductive Inductive types (HIIT) from Homotopy Type Theory [HoTT,
2013] provide another construction, in only one step and without the need for
an axiom of choice to prove completeness. The construction and the proof that
it produces an Archimedean ordered field were outlined in the HoTT book,
however formalization in the Coq proof assistant would have required
workarounds for the lack of inductive-inductive types until an experimental
branch by M. Sozeau started in 2015.

In section 2 we define a notion of _premetric space_ , which on the meta level
is a generalization of a metric space. From this we can define basic notions
such as Lipschitz functions and limits of Cauchy sequences (or rather the
equivalence but easier to work with Cauchy approximations).

Section 3 generalizes the construction of the Cauchy completion of rationals
from the HoTT book to arbitrary premetric spaces. This generalization shows
that Cauchy completion is a monadic operator on premetric spaces (where the
arrows are Lipschitz functions).

Lemmas relating to the specific structure of Cauchy reals (such as lemmas
about the order on reals) are retained as shown in section 4. The monadic
structure also provides a more natural way to define multiplication than that
used in HoTT [2013].

In section 5 we investigate how partial functions as per Partiality, Revisited
[2016] can be defined on our definition of Cauchy reals through the example of
a semi-decision procedure for the property $0<x$.

##  2 Premetric spaces

We follow OConnor07 [2007] in defining distance as a relation expressing when
two elements are sufficiently close. For O’Connor a metric space is a space
with a relation $B_{\varepsilon}(x,y)$ where $x$ and $y$ are elements of the
space and $\varepsilon:\mathbb{Q}^{+}$, which is interpreted as
$d(x,y)\leq\varepsilon$.

In contrast, HoTT [2013] defines a relation $x\approx_{\varepsilon}y$ for $x$
and $y$ Cauchy reals which is interpreted as $d(x,y)<\varepsilon$. We follow
HoTT in using the strict order $<$.

######  Definition 2.1 (Premetric space).

A _premetric space_ is a type $A$ together with a parametric mere relation
$\\_\approx_{\\_}\\_:\mathbb{Q}^{+}\rightarrow A\rightarrow A\rightarrow Prop$
verifying the following properties:

  * •

reflexivity:
$\forall(\varepsilon:\mathbb{Q}^{+})(x:A),x\approx_{\varepsilon}x$

  * •

symmetry:
$\forall(\varepsilon:\mathbb{Q}^{+})(x\;y:A),x\approx_{\varepsilon}y\rightarrow
y\approx_{\varepsilon}x$

  * •

separatedness: $\forall
x\;y:A,(\forall\varepsilon:\mathbb{Q}^{+},x\approx_{\varepsilon}y)\rightarrow
x=_{A}y$

  * •

triangularity:
$\forall(x\;y\;z:A)(\varepsilon\;\delta:\mathbb{Q}^{+}),x\approx_{\varepsilon}y\rightarrow
y\approx_{\delta}z\rightarrow x\approx_{\varepsilon+\delta}z$

  * •

roundedness:
$\forall(\varepsilon:\mathbb{Q}^{+})(x\;y:A),x\approx_{\varepsilon}y\leftrightarrow\exists\delta:\mathbb{Q}^{+},\delta<\varepsilon\wedge
x\approx_{\delta}y$

$\approx$ is called the closeness relation of $A$, with
$x\approx_{\varepsilon}y$ read as "$x$ and $y$ are $\varepsilon$-close" or
"the distance between $x$ and $y$ is less than $\varepsilon$".

######  Remark 2.2.

Classically, we can take
$d(x,y)=\sup\\{\varepsilon:\mathbb{Q}^{+},x\approx_{\varepsilon}y\\}$ with
values in $\mathbb{R}+\\{\infty\\}$ to turn a premetric space into a metric
space.

If we remain constructive, we expect a need for a locatedness property such as
$\forall(x\;y:A)\;(q\;r:\mathbb{Q}^{+}),q<r\rightarrow x\approx_{r}y\vee
x\not\approx_{q}y$.

We have not carried out the constructions due to lack of time, so these may
not be the exact properties required. For instance without countable choice
the position of the truncation may need to be different: this can be seen in
HoTT [2013] lemma 11.4.1.

We now work in an arbitrary premetric space $A$.

######  Definition 2.3 (Cauchy approximation).

$\operatorname{Approximation}A\coloneqq\Sigma_{x:\mathbb{Q}^{+}\rightarrow
A}\forall\varepsilon\;\delta:\mathbb{Q}^{+},x_{\varepsilon}\approx_{\varepsilon+\delta}x_{\delta}$

A Cauchy approximation $x:\operatorname{Approximation}A$ can be seen as a
function which given $\varepsilon$ produces a value at distance up to
$\varepsilon$ of an hypothetical limit.

By abuse of notation we confuse $x:\operatorname{Approximation}A$ with its
first projection.

######  Definition 2.4 (Limit).

$l:A$ is a limit of the approximation $x$ when

$\forall\varepsilon,\delta:\mathbb{Q}^{+},x_{\varepsilon}\approx_{\varepsilon+\delta}l$

Since we want to express $d(x_{\varepsilon},l)\leq\varepsilon$ but closeness
is interpreted as $<$ we introduce an additional $\delta$.

######  Lemma 2.5.

Limits are unique: if $l_{1}$ and $l_{2}$ are limits of
$x:\operatorname{Approximation}A$ then $l_{1}=l_{2}$.

We may then talk about _the_ limit of an approximation.

###### Proof.

By separatedness and triangularity. ∎

######  Definition 2.6 (Cauchy completeness).

$A$ is Cauchy complete when every Cauchy approximation has a limit. Since the
limit is unique, this is equivalent to having a function

$lim:\operatorname{Approximation}A\rightarrow A$

producing the limit for every approximation.

######  Theorem 2.7.

Rationals form a premetric space with
$q\approx_{\varepsilon}r\coloneqq|q-r|<\varepsilon$ as its closeness.

The following lemmas make working with limits easier.

######  Lemma 2.8.

Let $y:\operatorname{Approximation}A$, $l_{y}$ and $x:A$ and $\varepsilon$ and
$\delta:\mathbb{Q}^{+}$ such that $l_{y}$ is the limit of $y$ and
$x\approx_{\varepsilon}y_{\delta}$. Then $x\approx_{\varepsilon+\delta}l_{y}$.

###### Proof.

First strengthen the hypothesis $x\approx_{\varepsilon}y_{\delta}$ by
roundedness, then finish with triangularity. ∎

######  Lemma 2.9.

Let $x$ and $y:\operatorname{Approximation}A$, and
$\varepsilon\;\delta\;\kappa:\mathbb{Q}^{+}$ such that
$x_{\delta}\approx_{\varepsilon}y_{\kappa}$, then if $l_{x}$ is the limit of
$x$ and $l_{y}$ is the limit of $y$,
$l_{x}\approx_{\varepsilon+\delta+\kappa}l_{y}$.

###### Proof.

By two applications of lemma 2.8. ∎

######  Lemma 2.10.

If $x\;y:\operatorname{Approximation}A$ and $\varepsilon:\mathbb{Q}^{+}$ are
such that
$\forall\delta\;\kappa:\mathbb{Q}^{+},x_{\kappa}\approx_{\varepsilon+\delta}y_{\kappa}$,
then for $l_{x}$ limit of $x$ and $l_{y}$ limit of $y$,
$\forall\delta:\mathbb{Q}^{+},l_{x}\approx_{\varepsilon+\delta}l_{y}$.

###### Proof.

Using lemma 2.9, since
$\varepsilon+\delta=(\varepsilon+\frac{\delta}{3})+\frac{\delta}{3}+\frac{\delta}{3}$.
∎

###  2.1 Continuity notions

We will be interested in certain properties of functions between premetric
spaces $A$ and $B$.

######  Definition 2.11 (Lipschitz function).

A function $f:A\rightarrow B$ is Lipschitz with constant $L:\mathbb{Q}^{+}$
when

$\forall(\varepsilon:\mathbb{Q}^{+})(x,y:A),x\approx_{\varepsilon}y\rightarrow
f\;x\approx_{L*\varepsilon}f\;y$

If $L$ is $1$ we say that $f$ is non-expanding.

######  Definition 2.12 (Continuous function).

A function $f:A\rightarrow B$ is continuous when

$\forall(\varepsilon:\mathbb{Q}^{+})(x:A),\exists\delta:\mathbb{Q}^{+},\forall
y:A,x\approx_{\delta}y\rightarrow f\;x\approx_{\varepsilon}f\;y$

######  Lemma 2.13.

Lipschitz functions are continuous.

###### Proof.

Using $\delta\coloneqq\frac{\varepsilon}{L}$. ∎

Premetric spaces with continuous functions form a category.

Premetric spaces with Lipschitz functions also form a category. Notably the
identity is non-expanding.

###  2.2 The premetric space of functions

Let $A$ a type and $B$ a premetric space.

######  Definition 2.14 (Closeness of functions).

$f\approx_{\varepsilon}g\coloneqq\exists\delta:\mathbb{Q}^{+},\delta<\varepsilon\wedge\forall
x:A,f\;x\approx_{\delta}f\;y$

This expresses that $d(f,g)=\sup\\{d(f\;x,g\;x)|x:A\\}$.

######  Lemma 2.15.

For $\varepsilon:\mathbb{Q}^{+}$ and $f\;g:A\rightarrow B$, if
$f\approx_{\varepsilon}g$ then $\forall x:A,f\;x\approx_{\varepsilon}g\;x$.

###### Proof.

By roundedness. ∎

######  Theorem 2.16.

$A\rightarrow B$ forms a premetric space. If $B$ is Cauchy complete then so is
$A\rightarrow B$, and the limit of
$s:\operatorname{Approximation}(A\rightarrow B)$ is $\lambda
y,lim\;(\lambda\varepsilon,s\;\varepsilon\;y)$.

######  Lemma 2.17 (Limit of Lipschitz functions).

Suppose $A$ is a premetric space and $B$ is Cauchy complete.

If $s:\operatorname{Approximation}(A\rightarrow B)$ is such that
$\forall\varepsilon:\mathbb{Q}^{+}$, $s\;\varepsilon$ is Lipschitz with
constant $L$, then $lim\;s$ is Lipschitz with constant $L$.

###### Proof.

Let $\varepsilon:\mathbb{Q}^{+}$ and $x\;y:A$ such that
$x\approx_{\varepsilon}y$. By roundedness there merely is
$\delta\;\kappa:\mathbb{Q}^{+}$ such that $\varepsilon=\delta+\kappa$ and
$x\approx_{\delta}y$.

By hypothesis $\forall\eta:\mathbb{Q}^{+},s_{\eta}\;x\approx_{L*\delta}y$,
then by roundedness
$\forall\eta\;\eta^{\prime}:\mathbb{Q}^{+},s_{\eta}\;x\approx_{L*\delta+\eta^{\prime}}s_{\eta}\;y$.

By lemma 2.10 and unfolding the definition of $\lim s$ we have
$\forall\eta:\mathbb{Q}^{+},\lim s\;x\approx_{L*\delta+\eta}\lim s\;y$, then
since $L*\varepsilon=L*\delta+L*\kappa$ we have $\lim
s\;x\approx_{L*\varepsilon}\lim s\;y$. ∎

##  3 Cauchy completion

###  3.1 Definition and eliminators

In classical logic, we define the completion of a metric space $T$ as the
quotient of the Cauchy sequences (or equivalently of Cauchy approximations) in
$T$ by the equivalence $\lim f=\lim g$ (or rather an equivalent statement
which doesn’t assume the limit is defined). The axiom of countable choice is
then used to prove that Cauchy approximations in the quotient have limits in
the quotient.

Using higher inductive types, we can instead define
$\operatorname{\mathcal{C}}T$ the free complete premetric space generated by
$T$. By unfolding this statement we can see what constructors it needs:

  * •

generated by $T$: so there is a constructor of type
$T\rightarrow\operatorname{\mathcal{C}}T$.

  * •

premetric space: so we need to construct the closeness relation, and truncate
$\operatorname{\mathcal{C}}T$ to make it separated.

  * •

Cauchy complete: there is a constructor of type
$\operatorname{Approximation}(\operatorname{\mathcal{C}}T)\rightarrow\operatorname{\mathcal{C}}T$.

######  Definition 3.1.

$\operatorname{\mathcal{C}}T$ has the following constructors

$\displaystyle\operatorname{\eta}$
$\displaystyle:T\rightarrow\operatorname{\mathcal{C}}T$ $\displaystyle\lim$
$\displaystyle:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)\rightarrow\operatorname{\mathcal{C}}T$

The constructors of the closeness relation and the path constructors for
$\operatorname{\mathcal{C}}T$ and its closeness construct proof-irrelevant
values. As such, we do not name them but instead give them as inference rules
in fig. 1.

$\forall\varepsilon:\mathbb{Q}^{+},x\approx_{\varepsilon}y$ $x=y$ |  $p,q:x\approx_{\varepsilon}y$ $p=q$
---|---
$q\approx_{\varepsilon}r$ $\operatorname{\eta}q\approx_{\varepsilon}\operatorname{\eta}r$ |  $x_{\delta}\approx_{\varepsilon-\delta-\kappa}y_{\kappa}$ $\lim x\approx_{\varepsilon}\lim y$
$\operatorname{\eta}q\approx_{\varepsilon-\delta}y_{\delta}$ $\operatorname{\eta}q\approx_{\varepsilon}\lim y$ |  $x_{\delta}\approx_{\varepsilon-\delta}\operatorname{\eta}r$ $\lim x\approx_{\varepsilon}\operatorname{\eta}r$
Figure 1: Proof irrelevant constructors of $\operatorname{\mathcal{C}}$

We can use an explicit $fix$ expression in Coq to define the fully general
induction principle with the type given in HoTT [2013], however it is only
used through the following functions.

######  Definition 3.2 (Simple $\operatorname{\mathcal{C}}-$induction).

Given a mere predicate $A:\operatorname{\mathcal{C}}T\rightarrow Prop$ such
that the hypotheses in fig. 2 are verified,

$\forall x:\operatorname{\mathcal{C}}T,A\;x$

$A\;(\operatorname{\eta}q)$ |  $\forall\varepsilon:\mathbb{Q}^{+},A\;x_{\varepsilon}$ $A\;(\lim x)$
---|---
Figure 2: Hypotheses for simple $\operatorname{\mathcal{C}}-$induction.

######  Definition 3.3 (Simple $\approx-$induction).

Given a mere predicate

$P:\mathbb{Q}^{+}\rightarrow\operatorname{\mathcal{C}}T\rightarrow\operatorname{\mathcal{C}}T\rightarrow
Prop$

such that the hypotheses in fig. 3 are verified,

$\forall\varepsilon\;x\;y,x\approx_{\varepsilon}y\rightarrow
P\;\varepsilon\;x\;y$

$q\approx_{\varepsilon}r$
$P\;\varepsilon\;(\operatorname{\eta}q)\;(\operatorname{\eta}r)$

$x_{\delta}\approx_{\varepsilon-\delta-\kappa}y_{\kappa}$
$P\;(\varepsilon-\delta-\kappa)\;x_{\delta}\;y_{\kappa}$
$P\;\varepsilon\;(\lim x)\;(\lim y)$

$\operatorname{\eta}q\approx_{\varepsilon-\delta}y_{\delta}$
$P\;(\varepsilon-\delta)\;(\operatorname{\eta}q)\;y_{\delta}$
$P\;\varepsilon\;(\operatorname{\eta}q)\;(\lim y)$

$x_{\delta}\approx_{\varepsilon-\delta}\operatorname{\eta}r$
$P\;(\varepsilon-\delta)\;x_{\delta}\;(\operatorname{\eta}r)$
$P\;\varepsilon\;(\lim x)\;(\operatorname{\eta}r)$

Figure 3: Hypotheses for simple $\approx-$induction.

######  Definition 3.4 (Mutual $\operatorname{\mathcal{C}}-$recursion).

Let $A:Type$, a mere predicate $\sim:\mathbb{Q}^{+}\rightarrow A\rightarrow
A\rightarrow Prop$ and functions

$\displaystyle f_{\eta}:T\rightarrow A$ $\displaystyle
f_{lim}:\forall(x:\operatorname{Approximation}(\operatorname{\mathcal{C}}T))(f_{x}:\mathbb{Q}^{+}\rightarrow
A),$
$\displaystyle(\forall(\varepsilon,\delta:\mathbb{Q}^{+}),f_{x}\;\varepsilon\sim_{\varepsilon+\delta}f_{x}\;\delta)\rightarrow
A$

If the hypotheses in fig. 4 are verified, then we have

$\displaystyle f:\operatorname{\mathcal{C}}T\rightarrow A$ $\displaystyle
f_{\approx}:\forall(x,y:\operatorname{\mathcal{C}}T)(\varepsilon:\mathbb{Q}^{+}),x\approx_{\varepsilon}y\rightarrow
f\;x\sim_{\varepsilon}f\;y$

such that

$\displaystyle f\;(\operatorname{\eta}q)\coloneqq f_{\eta}\;q$ $\displaystyle
f\;(\lim x)\coloneqq f_{lim}\;x\;(f\circ
x)\;\left(\lambda\varepsilon\;\delta,f_{\approx}\;(\varepsilon+\delta)\;x_{\varepsilon}\;y_{\delta}\right)$

$\forall\varepsilon:\mathbb{Q}^{+},x\sim_{\varepsilon}y$ $x=y$

$q\approx_{\varepsilon}r$ $f_{\eta}\;q\sim_{\varepsilon}f_{\eta}\;r$ |  $f_{x}\;\delta\sim_{\varepsilon-\delta-\kappa}f_{y}\;\kappa$ $f_{lim}\;x\;f_{x}\;H_{x}\sim_{\varepsilon}f_{lim}\;y\;f_{y}\;H_{y}$
---|---

$f_{\eta}\;q\sim_{\varepsilon-\delta}f_{y}\;\delta$ $f_{\eta}\;q\sim_{\varepsilon}f_{lim}\;y\;f_{y}\;H_{y}$ |  $f_{x}\;\delta\sim_{\varepsilon-\delta}f_{\eta}\;r$ $f_{lim}\;x\;f_{x}\;H_{x}\sim_{\varepsilon}f_{\eta}\;r$
---|---

Figure 4: Hypotheses for mutual $\operatorname{\mathcal{C}}-$recursion.

###  3.2 Properties of the completion

We now seek to

  * •

show that $\operatorname{\mathcal{C}}T$ is indeed a premetric space, and that
$\lim$ constructs limits.

  * •

characterize the closeness relation: for instance
$\operatorname{\eta}q\approx_{\varepsilon}\operatorname{\eta}r$ should be
equivalent to $q\approx_{\varepsilon}r$.

Constructors of $\approx$ give us separatedness and proof irrelevance.

######  Lemma 3.5 (Reflexivity).

$\forall(u:\operatorname{\mathcal{C}}T)(\varepsilon:\mathbb{Q}^{+}),u\approx_{\varepsilon}u$

###### Proof.

By simple induction on $u$:

  * •

Let $u:T$ and $\varepsilon:\mathbb{Q}^{+}$. $T$ is a premetric space so
$u\approx_{\varepsilon}u$, then
$\operatorname{\eta}u\approx_{\varepsilon}\operatorname{\eta}u$.

  * •

Let $x:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)$ such that

$\forall(\varepsilon,\delta:\mathbb{Q}^{+}),x_{\varepsilon}\approx_{\delta}x_{\varepsilon}$

Let $\varepsilon:\mathbb{Q}^{+}$. Then
$x_{\varepsilon/3}\approx_{\varepsilon/3}x_{\varepsilon/3}$, so $\lim
x\approx_{\varepsilon}\lim x$.

∎

######  Lemma 3.6.

$\operatorname{\mathcal{C}}T$ is a set.

###### Proof.

By HoTT [2013] theorem 7.2.2 and separatedness. ∎

######  Lemma 3.7 (Symmetry).

$\forall(\varepsilon:\mathbb{Q}^{+})(xy:\operatorname{\mathcal{C}}T),x\approx_{\varepsilon}y\rightarrow
y\approx_{\varepsilon}x$

###### Proof.

By simple $\approx-$induction, since $T$ has a symmetric closeness relation. ∎

To go further we need a way to deconstruct proofs of closeness. This is done
by defining a function
$B_{\\_}(\\_,\\_):\mathbb{Q}^{+}\rightarrow\operatorname{\mathcal{C}}T\rightarrow\operatorname{\mathcal{C}}T\rightarrow
Prop$ recursively on the two $\operatorname{\mathcal{C}}T$ arguments which is
equivalent to $\approx$.

$B$ will be defined by mutual $\operatorname{\mathcal{C}}-$recursion as it is
proof-relevant. In order to be able to prove the side conditions we will first
inhabit a subtype then obtain $B$ by projection.

######  Definition 3.8 (Concentric balls).

A set of concentric balls is a value of type

$Balls\coloneqq\Sigma_{B:\operatorname{\mathcal{C}}T\rightarrow\mathbb{Q}^{+}\rightarrow
Prop}\\\ \left(\forall
y\;\varepsilon,B_{\varepsilon}\;y\leftrightarrow\exists\delta<\varepsilon,B_{\delta}\;y\right)\\\
\wedge\left(\forall\varepsilon\;\delta\;y\;z,y\approx_{\varepsilon}z\rightarrow
B_{\delta}\;y\rightarrow B_{\delta+\varepsilon}\;z\right)$

We call the first property _ball roundedness_ , and the second _ball
triangularity_.

For $\varepsilon:\mathbb{Q}^{+}$ and $B_{1},B_{2}:Balls$, let
$B_{1}\approx_{\varepsilon}B_{2}$ when for $\\{i,j\\}=\\{1,2\\}$

$\forall
y\;\delta,{B_{i}}_{\delta}\;y\rightarrow{B_{j}}_{\delta+\varepsilon}\;y$

######  Definition 3.9 (Upper cut).

An upper cut is a predicate on $\mathbb{Q}^{+}$ which is upward rounded, i.e.

$Upper\coloneqq\Sigma_{U:\mathbb{Q}^{+}\rightarrow
Prop}\left(\forall\varepsilon,U_{\varepsilon}\leftrightarrow\exists\delta<\varepsilon,U_{\delta}\right)$

For $\varepsilon:\mathbb{Q}^{+}$ and $U_{1},U_{2}:Upper$, let
$U_{1}\approx_{\varepsilon}U_{2}$ when for $\\{i,j\\}=\\{1,2\\}$

$\forall\delta,{U_{i}}_{\delta}\rightarrow{U_{j}}_{\delta+\varepsilon}$

######  Lemma 3.10.

The closeness on $Balls$ is separated.

###### Proof.

Let $B^{(1)},B^{(2)}:Balls$ such that $B^{(1)}$ and $B^{(2)}$ are
$\varepsilon-$close for all $\varepsilon$. Let $\varepsilon$ and $y$, we need
$B^{(1)}_{\varepsilon}\;y=B^{(2)}_{\varepsilon}\;y$. By univalence this is
$B^{(1)}_{\varepsilon}\;y\leftrightarrow B^{(2)}_{\varepsilon}\;y$.

Suppose $B^{(1)}_{\varepsilon}\;y$, by ball roundedness there merely is
$\delta<\varepsilon$ such that $B^{(1)}_{\delta}\;y$. $B^{(1)}$ and $B^{(2)}$
are $(\varepsilon-\delta)-$close, so we have $B^{(2)}_{\varepsilon}\;y$.

The second direction is the same by symmetry. ∎

######  Lemma 3.11.

The closeness on $Upper$ is separated.

###### Proof.

Like with lemma 3.10 we use first roundedness then the definition of upper cut
closeness at the appropriate $\varepsilon-\delta$. ∎

######  Lemma 3.12 (Concentric balls from upper cuts).

Suppose $B:\operatorname{\mathcal{C}}T\rightarrow Upper$ is non-expanding,
then the underlying
$\operatorname{\mathcal{C}}T\rightarrow\mathbb{Q}^{+}\rightarrow Prop$ is a
set of concentric balls

###### Proof.

Ball roundedness property is exactly upper cut roundedness.

$B$ verifies ball triangularity because it is non-expanding. ∎

######  Definition 3.13 (Balls around a base element).

Let $q:T$. The set of concentric balls around $q$ is
$B_{\\_}(\operatorname{\eta}q,\\_)$ defined by mutual
$\operatorname{\mathcal{C}}-$recursion as a non-expanding function of type
$\operatorname{\mathcal{C}}T\rightarrow Upper$ suitable for lemma 3.12.

The proof relevant values are as follows:

  * •

base case:
$B_{\varepsilon}(\operatorname{\eta}q,\operatorname{\eta}r)\coloneqq
q\approx_{\varepsilon}r$. This produces an upper cut by roundedness of $T$.

  * •

limit case: $B_{\varepsilon}(\operatorname{\eta}q,\lim
x)\coloneqq\exists\delta<\varepsilon,B_{\varepsilon-\delta}(\operatorname{\eta}q,x_{\delta})$.
This produces an upper cut by the induction hypothesis and roundedness at the
recursive call.

The remaining hypotheses expressing that the construction is non-expanding are
hard to see through on paper. In Coq however reduction makes how to proceed
obvious. Let us consider the $\eta-lim$ case.

Let $q\;r:T$, $\varepsilon\;\delta:\mathbb{Q}^{+}$ such that
$\delta<\varepsilon$, and
$y:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)$ such that we
have $\lambda\kappa\;\xi,B_{\xi}(\operatorname{\eta}q,y_{\kappa})$. This later
function is an approximation on upper cuts. Finally the induction hypothesis
is that
$\left(\lambda\kappa,q\approx_{\kappa}r\right)\approx_{\varepsilon-\delta}\left(\lambda\kappa,B_{\kappa}(\operatorname{\eta}q,x_{\delta})\right)$
as upper cuts.

In that context, we need to prove that
$\left(\lambda\kappa,q\approx_{\kappa}r\right)\approx_{\varepsilon}\left(\lambda\kappa,B_{\kappa}(\operatorname{\eta}q,\lim
x)\right)$ as upper cuts. Let $\kappa:\mathbb{Q}^{+}$, we have two goals:

  * •

If $q\approx_{\kappa}r$ then $B_{\kappa+\varepsilon}(\operatorname{\eta}q,\lim
x)$ i.e.

$\exists\delta<\kappa+\varepsilon,B_{\kappa+\varepsilon-\delta}(\operatorname{\eta}q,x_{\delta})$

By the induction hypothesis and $q\approx_{\kappa}r$ we have

$B_{\varepsilon-\delta+\kappa}(\operatorname{\eta}q,x_{\delta})$

with $\delta<\varepsilon<\varepsilon+\kappa$.

  * •

If $\exists xi<\kappa,B_{\kappa-\xi}(\operatorname{\eta}q,x_{\xi})$ then
$q\approx_{\kappa+\varepsilon}r$.
Because $\lambda\kappa\;\xi,B_{\xi}(\operatorname{\eta}q,y_{\kappa})$ is a cut
approximation we have
$B_{\kappa-\xi+\delta+\xi}(\operatorname{\eta}q,x_{\delta})=B_{\kappa+\delta}(\operatorname{\eta}q,x_{\delta})$.
Then by induction hypothesis $q\approx_{\kappa+\varepsilon}r$.

We then similarly define the concentric balls around a limit point, and show
that this definition and definition 3.13 respect $\approx$ using simple
$\operatorname{\mathcal{C}}-$induction. In order to have space for more
interesting proofs we shall simply recap what results we obtain from this
process.

######  Theorem 3.14.

We have for all $(\varepsilon:\mathbb{Q}^{+})$ and
$x\;y:\operatorname{\mathcal{C}}T$, $B_{\varepsilon}(x,y):Prop$ such that
$\lambda x\;y\;\varepsilon,B_{\varepsilon}(x,y)$ is a non-expanding function
from $\operatorname{\mathcal{C}}T$ to $Balls$. Additionally we have the
following computation rules:

$\displaystyle
B_{\varepsilon}(\operatorname{\eta}q,\operatorname{\eta}r)\coloneqq
q\approx_{\varepsilon}r$ $\displaystyle
B_{\varepsilon}(\operatorname{\eta}q,\lim
y)\coloneqq\exists\delta<\varepsilon,B_{\varepsilon-\delta}(\operatorname{\eta}q,y_{\delta})$
$\displaystyle B_{\varepsilon}(\lim
x,\operatorname{\eta}r)\coloneqq\exists\delta<\varepsilon,B_{\varepsilon-\delta}(x_{\delta},\operatorname{\eta}r)$
$\displaystyle B_{\varepsilon}(\lim x,\lim
y)\coloneqq\exists\delta+\kappa<\varepsilon,B_{\varepsilon-\delta-\kappa}(x_{\delta},y_{\kappa})$

######  Theorem 3.15.

$B_{\varepsilon}(x,y)$ and $x\approx_{\varepsilon}y$ are equivalent.

###### Proof.

We prove both sides of the equivalence separately:

  * •

$\forall(u,v:\operatorname{\mathcal{C}}T)(\varepsilon:\mathbb{Q}^{+}),B_{\varepsilon}(u,v)\rightarrow
u\approx_{\varepsilon}v$
By simple induction on $u$ then $v$, then using the computation rules of $B$
and the constructors of $\approx$.

  * •

$\forall(\varepsilon:\mathbb{Q}^{+})(u,v:\operatorname{\mathcal{C}}T),u\approx_{\varepsilon}v\rightarrow
B_{\varepsilon}(u,v)$
By simple $\approx-$induction, with each case being trivial.

∎

We can now use the computation rules in theorem 3.14 as computation rules for
$\approx$.

######  Theorem 3.16.

$\operatorname{\mathcal{C}}T$ forms a premetric space.

###### Proof.

Roundedness of $B$ as a closeness relation is obtained from roundedness as a
function into $Balls$, then we use that $B$ equals $\approx$ to have
roundedness of $\approx$.

The triangularity property of $B$ as a function into balls together with
theorem 3.15 shows that $\approx$ is triangular.

Separatedness comes by definition of $\operatorname{\mathcal{C}}T$, and the
other properties of a premetric space are already proven in lemmas 3.7 and
3.5. ∎

######  Corollary 3.17.

$\operatorname{\eta}$ is injective.

###### Proof.

By separatedness. ∎

######  Theorem 3.18.

$\operatorname{\mathcal{C}}T$ is Cauchy complete, i.e. for all
$x:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)$, $\lim x$ is the
limit of $x$.

###### Proof.

Lemma 2.8 also holds for $\operatorname{\mathcal{C}}T$:

$\forall(u:\operatorname{\mathcal{C}}T)(y:\operatorname{Approximation}(\operatorname{\mathcal{C}}T))(\varepsilon,\delta:\mathbb{Q}^{+}),\\\
u\approx_{\varepsilon}y_{\delta}\rightarrow u\approx_{\varepsilon+\delta}\lim
y$

By simple induction on $u$:

  * •

Let $v:T,y:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)$ and
$\varepsilon,\delta:\mathbb{Q}^{+}$ such that
$\operatorname{\eta}v\approx_{\varepsilon}y_{\delta}$.
Then by constructor $\operatorname{\eta}v\approx_{\varepsilon+\delta}\lim y$.

  * •

Let $x:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)$ such that
(induction hypothesis)

$\forall(\varepsilon_{0},\varepsilon,\delta:\mathbb{Q}^{+})(y:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)),\\\
x_{\varepsilon_{0}}\approx_{\varepsilon}y_{\delta}\rightarrow
x_{\varepsilon_{0}}\approx_{\varepsilon+\delta}\lim y$

and let $y,\varepsilon,\delta$ such that $\lim
x\approx_{\varepsilon}y_{\delta}$.
By roundedness, there merely exist $\kappa,\theta:\mathbb{Q}^{+}$ such that
$\varepsilon=\kappa+\theta$ and $\lim x\approx_{\kappa}y_{\delta}$.
The induction hypothesis used with $y\coloneqq x$ and reflexivity of $\approx$
gives that
$\forall(\varepsilon,\delta:\mathbb{Q}^{+}),x_{\varepsilon}\approx_{\varepsilon+\delta}\lim
x$ (i.e. $\lim x$ is the limit of $x$). Specifically,
$x_{\theta/4}\approx_{3\theta/4}\lim x$.
By triangularity, $x_{\theta/4}\approx_{3\theta/4+\kappa}y_{\delta}$.
By constructor $\lim x\approx_{\theta+\kappa+\delta}\lim y$.
Then $\lim x\approx_{\varepsilon+\delta}\lim y$.

Then using this result and lemma 3.7 shows that $\lim x$ is the limit of $x$.
∎

###  3.3 Monadic structure of the completion

Continuity lets us characterize functions on $\operatorname{\mathcal{C}}T$
based on their behaviour on the base elements $\operatorname{\eta}x$. If a
function is sufficiently continuous, i.e. Lipschitz, we can even define its
value on $\operatorname{\mathcal{C}}T$ from its value on $T$: this turns the
completion into a monad.

######  Theorem 3.19.

Let $A$ a premetric space and $f,g:\operatorname{\mathcal{C}}T\rightarrow A$
continuous functions such that

$\forall u:T,f\;(\operatorname{\eta}u)=g\;(\operatorname{\eta}u)$

Then

$\forall x:\operatorname{\mathcal{C}}T,f\;x=g\;x$

###### Proof.

By induction on $x$ (the desired property is a mere proposition because
premetric spaces are sets). The base case is trivial.

Let $x:\operatorname{Approximation}(\operatorname{\mathcal{C}}T)$ with the
induction hypothesis

$\forall\varepsilon:\mathbb{Q}^{+},f\;x_{\varepsilon}=g\;x_{\varepsilon}$

By separatedness it suffices to prove that

$\forall\varepsilon:\mathbb{Q}^{+},f(\lim x)\approx_{\varepsilon}g(\lim x)$

Let $\varepsilon:\mathbb{Q}^{+}$. Continuity of $f$ and $g$ at $\lim x$ and
$\varepsilon/2$ shows that there merely exist $\delta_{f}$ and
$\delta_{g}:\mathbb{Q}^{+}$ such that

$\forall y:\operatorname{\mathcal{C}}T,\lim x\approx_{\delta_{f}}y\rightarrow
f(\lim x)\approx_{\varepsilon/2}f\;y$ $\forall
y:\operatorname{\mathcal{C}}T,\lim x\approx_{\delta_{g}}y\rightarrow g(\lim
x)\approx_{\varepsilon/2}g\;y$

Let $\delta:\mathbb{Q}^{+}$ such that $\delta<\delta_{f}$ and $\delta_{g}$. By
roundedness and because $\lim x$ is the limit of $x$, $\lim
x\approx_{\delta_{f}}x_{\delta}$ and $\lim x\approx_{\delta_{g}}x_{\delta}$.

Then $f\;(\lim x)\approx_{\varepsilon/2}f\;x_{\delta}=g\;x_{\delta}$ and
$g\;(\lim x)\approx_{\varepsilon/2}g\;x_{\delta}$.

By triangularity $f\;(\lim x)\approx_{\varepsilon}g\;(\lim x)$. ∎

Repeated application of theorem 3.19 lets us deal with multiple variables. For
instance, if $f$ and
$g:\operatorname{\mathcal{C}}T_{1}\rightarrow\operatorname{\mathcal{C}}T_{2}\rightarrow
A$ are continuous in both arguments (i.e. for all $x$, $f\;x$ and $g\;x$ are
continuous, and for all $y$, $\lambda x,f\;x\;y$ and $\lambda x,g\;x\;y$ are
continuous) and they coincide on $T_{1}$ and $T_{2}$ then they are equal.

######  Theorem 3.20.

Let $A$ a Cauchy complete premetric space and $f:T\rightarrow A$ Lipschitz
with constant $L$. There exists
$\overline{f}:\operatorname{\mathcal{C}}T\rightarrow A$ Lipschitz with
constant $L$ such that

$\forall x:T,\overline{f}(\operatorname{\eta}x)=f\;x$

###### Proof.

We define $\overline{f}:\operatorname{\mathcal{C}}T\rightarrow A$ by mutual
recursion, guaranteeing that the images of $\varepsilon$-close values are
$L*\varepsilon$-close. This condition is exactly that $\overline{f}$ is
Lipschitz with constant $L$.

In the base case we simply use $f$.

In the limit case, the induction hypothesis is
$\overline{f_{x}}:\mathbb{Q}^{+}\rightarrow A$ such that

$\forall\varepsilon,\delta:\mathbb{Q}^{+},\overline{f_{x}}\;\varepsilon\approx_{L*(\varepsilon+\delta)}\overline{f_{x}}\;\delta$

Then $\lambda\varepsilon,\overline{f_{x}}\;(\varepsilon/L)$ is a Cauchy
approximation and we take its limit.

The coherence properties necessary for mutual recursion are easy given lemmas
2.8 and 2.9. ∎

######  Theorem 3.21.

If $T$ is Cauchy complete then $\operatorname{\mathcal{C}}T=T$.

###### Proof.

The identity of $T$ is non-expanding, so it can be extended into
$\overline{id_{T}}:\operatorname{\mathcal{C}}T\rightarrow T$.

$\overline{id_{T}}\circ\operatorname{\eta}_{T}$ is convertible to $id_{T}$.

$\operatorname{\eta}_{T}\circ\overline{id_{T}}=id_{\operatorname{\mathcal{C}}T}$
by continuity.

Then $\overline{id_{T}}$ is an equivalence from $\operatorname{\mathcal{C}}T$
to $T$, and by univalence they are equal. ∎

The above result uses univalence to get a strong identity result as opposed to
the more common isomorphism. Note however that we do not get an isomorphism
without univalence: the identity
$\operatorname{\eta}_{T}\circ\overline{id_{T}}=id_{\operatorname{\mathcal{C}}T}$
is proven by theorem 3.19 at $A\coloneqq\operatorname{\mathcal{C}}T$. To know
that $\operatorname{\mathcal{C}}T$ is a premetric space we need theorem 3.14,
which needs univalence to show that it preserves equality (in lemma 3.10).

######  Theorem 3.22.

The Cauchy completion is an idempotent monad on the category of premetric
spaces with Lipschitz functions.

###### Proof.

Given $f:A\rightarrow B$ a Lipschitz function with constant $L$,
$\operatorname{\eta}\circ f:A\rightarrow\operatorname{\mathcal{C}}B$ and
$\overline{\operatorname{\eta}\circ
f}:\operatorname{\mathcal{C}}A\rightarrow\operatorname{\mathcal{C}}B$ are
Lipschitz functions with constant $L$.

The identities about extension of identity and extension of composition are
verified by continuity.

Then completion is a functor, and the previous theorem shows it is an
idempotent monad. ∎

######  Remark 3.23.

OConnor07 [2007] defines Cauchy completion as a monad on the category of
metric spaces with uniformly continuous functions (with setoid identities).
However the map operation requires the domain to have the additional
_prelength space_ property (reversed triangularity:
$\forall\varepsilon\;\delta\;a\;c,a\approx_{\varepsilon+\delta}c\rightarrow\exists
b,a\approx_{\varepsilon}b\wedge b\approx_{\delta}c$) to be well-defined. It
therefore seems that restricting the arrows to Lipschitz functions spared us
from having to define and work with this property.

Repeated Lipschitz extension can be applied to functions taking multiple
arguments: if $f:A\rightarrow B\rightarrow T$ is Lipschitz in both arguments,
the function $f_{1}:A\rightarrow\operatorname{\mathcal{C}}B\rightarrow T$
obtained by pointwise Lipschitz extension is itself a Lipschitz function into
the Cauchy complete space $\operatorname{\mathcal{C}}B\rightarrow T$.

######  Lemma 3.24.

If $A$ is Cauchy complete and $f,g:T\rightarrow A$ are Lipschitz functions
with constant $L$ and $\varepsilon:\mathbb{Q}^{+}$ is such that

$\forall(u:T)(\delta:\mathbb{Q}^{+}),f\;u\approx_{\varepsilon+\delta}g\;u$

Then

$\forall(u:\operatorname{\mathcal{C}}T)(\delta:\mathbb{Q}^{+}),\overline{f}\;u\approx_{\varepsilon+\delta}\overline{g}\;u$

###### Proof.

By simple induction on $u$, using lemma 2.10 in the limit case. ∎

######  Theorem 3.25 (Binary Lipschitz extension).

If $T$ is Cauchy complete and $f:A\rightarrow B\rightarrow T$ is such that for
all $x:A$, $f\;x\;\\_$ is Lipschitz with constant $L_{1}$ and for all $y:B$,
$f\;\\_\;y$ is Lipschitz with constant $L_{2}$, then $f$ can be extended into
$\overline{\overline{f}}:\operatorname{\mathcal{C}}A\rightarrow\operatorname{\mathcal{C}}B\rightarrow
T$ with the same Lipschitz properties and coinciding with $f$ on
$\operatorname{\eta}$ values.

###### Proof.

Unary Lipschitz extension gives us $f_{1}\coloneqq\lambda
x,\overline{f\;x}:A\rightarrow\operatorname{\mathcal{C}}B\rightarrow T$ such
that for all $x:A$, $f_{1}\;x\;\\_$ is Lipschitz with constant $L1$.

$f_{1}$ is Lipschitz with constant $L_{2}$: let $\varepsilon:\mathbb{Q}^{+}$
and $x,y:A$ such that $x\approx_{\varepsilon}y$. We need to show that
$f_{1}\;x\approx_{L_{2}*\varepsilon}f_{1}\;y$, i.e. there merely exist
$\delta_{1},\kappa_{1}:\mathbb{Q}^{+}$ such that
$L_{2}*\varepsilon=\delta_{1}+\kappa_{1}$ and $\forall
z:B,\overline{f\;x}\;z\approx_{\delta_{1}}\overline{f\;y}\;z$.

By roundedness there merely exist $\delta,\kappa:\mathbb{Q}^{+}$ such that
$\varepsilon=\delta+\kappa$ and $x\approx_{\delta}y$. Use $\delta_{1}\coloneqq
L_{2}*\delta$ and $\kappa_{1}\coloneqq L_{2}*\kappa$.

By roundedness there merely exist
$\delta^{\prime},\kappa^{\prime}:\mathbb{Q}^{+}$ such that
$\delta=\delta^{\prime}+\kappa^{\prime}$ and $x\approx_{\delta^{\prime}}y$. By
lemma 3.24 it suffices to prove

$\forall(z:B)(\theta:\mathbb{Q}^{+}),f\;x\;z\approx_{L_{2}*\delta^{\prime}+\theta}f\;y\;z$

Since $f\;\\_\;z$ is Lipschitz with constant $L_{2}$ we have

$f\;x\;z\approx_{L_{2}*\delta^{\prime}}f\;y\;z$

then by roundedness the desired property.

$\operatorname{\mathcal{C}}B\rightarrow T$ is Cauchy complete, so we have
$\overline{\overline{f}}\coloneqq\overline{f_{1}}:\operatorname{\mathcal{C}}A\rightarrow\operatorname{\mathcal{C}}B\rightarrow
T$ Lipschitz with constant $L_{2}$.

By lemma 2.15 we have that for all $y:\operatorname{\mathcal{C}}B$,
$\overline{\overline{f}}\;\\_\;y$ is Lipschitz with constant $L_{2}$.

By $\operatorname{\mathcal{C}}$-induction and lemma 2.17 we have that for all
$x:\operatorname{\mathcal{C}}A$, $\overline{\overline{f}}\;x\;\\_$ is
Lipschitz with constant $L_{1}$. ∎

##  4 Cauchy reals

We now have enough to define concepts specific to the Cauchy completion of the
rationals, i.e. the Cauchy reals. Our goal is to show that they form an
archimedean ordered field, a lattice, and that the closeness relation has the
intended meaning $x\approx_{\varepsilon}y\leftrightarrow|x-y|<\varepsilon$
(with absolute value of $x$ being the join of $x$ and $-x$).

Note that we use the constructive sense of ordered field, such that we have an
apartness relation $x\operatorname{\\#}y$ expressing $0<|x-y|$ and
multiplicative inverse can only be applied on values apart from $0$.

###  4.1 Addition and order relations

The Cauchy reals are the Cauchy completion of the rationals
$\operatorname{\mathcal{C}}\mathbb{Q}$. Let
$\operatorname{rat}:\mathbb{Q}\rightarrow\mathbb{R}_{c}$ be an alias for
$\operatorname{\eta}$.

We follow HoTT [2013] for the additive and order structure of : $0$ is
$\operatorname{rat}0_{\mathbb{Q}}$, $1$ is $\operatorname{rat}0_{\mathbb{Q}}$,
and $+$, $-$, $\cup$, $\cap$ and $|\\_|$ are defined by Lipschitz extension.

The HoTT book states:

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

This is a simple application of theorem 3.19. More complex uses need us to pay
a little more attention to two issues:

  * •

Consider transitivity of $\leq$:

$\forall x\;y\;z:\real,x\cup y=y\rightarrow y\cup z=z\rightarrow x\cup z=z$

This cannot be directly proven by continuity as the statement of theorem 3.19
does not allow for hypotheses which depend on the universally quantified
variables.

We can however strengthen this specific statement into one that can be solved
by theorem 3.19: $\forall x\;y\;z:\real,x\cup((x\cup y)\cup z)=(x\cup y)\cup
z$. Doing this strengthening when we wish to use theorem 3.19 has not been an
issue, but it is unclear where it might be a problem and so should be kept in
mind.

  * •

When showing that is a group we need to prove $\forall x:\real,x+(-x)=0$.

The issue is that for a binary function $f:A\rightarrow B\rightarrow C$,
knowing that for all $x$ and $y$ $\lambda y,f\;x\;y$ and $\lambda x,f\;x\;y$
are continuous is not sufficient to show that $\lambda x,f\;x\;x$ is
continuous. The hypothesis we really want is that $f$ as the uncurried
function from $A\times B$ to $C$ is continuous.

If $\lambda y,f\;x\;y$ and $\lambda x,f\;x\;y$ are both Lipschitz with
respective constant $L$ and $K$ then $f$ is Lipschitz with constant $L+K$, so
this is not a problem when dealing with functions defined through Lipschitz
extension like addition. However, showing that multiplication is continuous as
an uncurried function deserves an explicit proof.

Except for those which have to do with multiplication, the proofs from HoTT
[2013] can be adapted with at most minor adjustments aside from the above
remarks. Then is a group, a lattice, $x\approx_{\varepsilon}y$ is equivalent
to $|x-y|<\varepsilon$, etc.

The book lacks the proof that $\lambda y,x+y$ preserves $<$. We show this by
proving that $x<y$ if and only if there merely is $\varepsilon:\mathbb{Q}^{+}$
such that $x+\operatorname{rat}\varepsilon\leq y$, which then allows us to use
properties proven by continuity.

######  Lemma 4.1.

Let $x,y:\real$ such that $x<y$. Then
$\exists\varepsilon:\mathbb{Q}^{+},x+\operatorname{rat}\varepsilon\leq y$.

###### Proof.

By definition of $<$ there merely are $q,r:\mathbb{Q}$ such that
$x\leq\operatorname{rat}q<\operatorname{rat}r\leq y$. We take
$\varepsilon\coloneqq r-q$.
$x\leq\operatorname{rat}q$ so

$x+\operatorname{rat}\varepsilon=\operatorname{rat}(r-q)+x\leq\operatorname{rat}(r-q)+\operatorname{rat}q=\operatorname{rat}r\leq
y$

∎

For the second direction, it is enough to show that
$x<x+\operatorname{rat}\varepsilon$. We need a helper lemma first.

######  Lemma 4.2.

Let $\varepsilon:\mathbb{Q}^{+}$ and $x,y:\real$ such that
$x\approx_{\varepsilon}y$. Then $y\leq x+\operatorname{rat}\varepsilon$.

###### Proof.

$y-x\leq|x-y|<\operatorname{rat}\varepsilon$ so $y\leq
x+\operatorname{rat}\varepsilon$. ∎

We can generalize HoTT [2013] lemma 11.3.43:

######  Lemma 4.3.

Let $x\;y\;z:\real$ and $\varepsilon:\mathbb{Q}^{+}$ such that $x<y$ and
$x\approx_{\varepsilon}z$. Then $z<y+\operatorname{rat}\varepsilon$.

###### Proof.

There merely is $q:\mathbb{Q}$ between $x$ and $y$. By HoTT [2013] lemma
11.3.43, $z<\operatorname{rat}(q+\varepsilon)\leq
y+\operatorname{rat}\varepsilon$.

Note here that we cannot prove
$\operatorname{rat}(q+\varepsilon)<y+\operatorname{rat}\varepsilon$ since
$\lambda u,u+\operatorname{rat}\varepsilon$ preserving $<$ is a future lemma.
∎

######  Lemma 4.4.

$<$ is cotransitive:

$\forall x,y,z:\real,x<y\rightarrow x<z\vee z<y$

Note that $\vee$ is the truncated disjunction, i.e. the case distinction can
only be made when proving a mere proposition.

###### Proof.

By definition of $<$ we can reduce to the case where
$x\coloneqq\operatorname{rat}q$ and $y\coloneqq\operatorname{rat}r$ for some
$q,r:\mathbb{Q}$. Then we use simple $\operatorname{\mathcal{C}}-$induction on
$z$.

In the base case, we inherit the property from $\mathbb{Q}$.

In the limit case, we have $x:\operatorname{Approximation}\real$ such that
(induction hypothesis)

$\forall(\varepsilon:\mathbb{Q}^{+})(q,r:\mathbb{Q}),q<r\rightarrow\operatorname{rat}q<x_{\varepsilon}\vee
x_{\varepsilon}<\operatorname{rat}r$

Let $q,r:\mathbb{Q}$ such that $q<r$. There are $q_{1},r_{1}:\mathbb{Q}$ such
that $q<q_{1}<r_{1}<r$, and $\delta:\mathbb{Q}^{+}$ such that $\delta<q_{1}-q$
and $\delta<r-r_{1}$.
Using the induction hypothesis with $\delta$ and $q_{1}<r_{1}$ we can do a
case distinction:

  * •

if $\operatorname{rat}q_{1}<x_{\delta}$, we have
$-x_{\delta}<\operatorname{rat}(-q_{1})$ and since
$x_{\delta}\approx_{q_{1}-q}\lim x$ and $-$ is non-expanding we have using
lemma 4.3 that $-\lim
x<\operatorname{rat}(-q_{1}+(q_{1}-q))=\operatorname{rat}(-q)$.

  * •

if $x_{\delta}<\operatorname{rat}r_{1}$ using lemma 4.3 we have $\lim
x<\operatorname{rat}(r_{1}+(r-r_{1}))=\operatorname{rat}r$.

∎

######  Lemma 4.5.

For all $x:\real$ and $\varepsilon:\mathbb{Q}^{+}$,
$x<x+\operatorname{rat}\varepsilon$.

###### Proof.

By simple $\operatorname{\mathcal{C}}-$induction on $x$.

In the base case we inherit the result from $\mathbb{Q}$.

In the limit case, let $x:\operatorname{Approximation}\real$ such that
(induction hypothesis)

$\forall\varepsilon,\delta:\mathbb{Q}^{+},x_{\varepsilon}<x_{\varepsilon}+\operatorname{rat}\delta$

Let $\varepsilon:\mathbb{Q}^{+}$. By lemma 4.3 and the induction hypothesis we
have $\forall\delta,\kappa:\mathbb{Q}^{+},\lim
x<x_{\delta}+\operatorname{rat}(\delta+\kappa)$.
Using $\delta\coloneqq\varepsilon/3$ and $\kappa\coloneqq 2\varepsilon/9$, by
cotransitivity of $<$ (HoTT [2013] lemma ) for $\lim
x+\operatorname{rat}\varepsilon$ we have either

  * •

$\lim x<\lim x+\operatorname{rat}\varepsilon$ as desired

  * •

$\lim
x+\operatorname{rat}\varepsilon<x_{\delta}+\operatorname{rat}(\delta+\kappa)$,
but this is absurd:
By lemma 4.2 $x_{\delta}\leq\lim x+\operatorname{rat}(\delta+\varepsilon/9)$,
then by adding $\delta+\kappa=11\varepsilon/9$ to both sides
$x_{\delta}+\operatorname{rat}(\delta+\kappa)\leq\lim
x+\operatorname{rat}\varepsilon<x_{\delta}+\operatorname{rat}(\delta+\kappa)$.

∎

We also need to prove $x\leq y$ from $\neg y<x$.

######  Lemma 4.6.

Real numbers can be approximated from below: let $x:\real$, then
$\lambda\varepsilon:\mathbb{Q}^{+},x-\operatorname{rat}\varepsilon$ is an
approximation with limit $x$.

###### Proof.

HoTT [2013] theorem 11.3.44 (expressing $x\approx_{\varepsilon}y$ as
$|x-y|<\operatorname{rat}\varepsilon$) lets us reduce this to bureaucratic
work. ∎

######  Lemma 4.7.

Let $f:\real\rightarrow\real$ Lipschitz with constant $L$ and
$x:\operatorname{Approximation}\real$. Then
$\lambda\varepsilon,f\;x_{\varepsilon/L}$ is an approximation with limit
$f\;(\lim x)$.

###### Proof.

Easy. ∎

######  Lemma 4.8.

Given $x,y:\real$, if $x<y$ is false then $y\leq x$.

###### Proof.

Let $x,y:\real$ such that $x<y$ is false. Let $z\coloneqq x-y$.

First note that
$\forall\varepsilon:\mathbb{Q}^{+},-\operatorname{rat}\varepsilon<z$: let
$\varepsilon:\mathbb{Q}^{+}$. Since $y-\operatorname{rat}\varepsilon<y$ by
cotransitivity either $y-\operatorname{rat}\varepsilon<x$ as desired, or $x<y$
which is absurd.

$y\leq x$ is equivalent to $0\leq z$ i.e. $0\cup z=z$. By lemma 4.6
$0=\lim(\lambda\varepsilon,-\operatorname{rat}\varepsilon)$ so by lemma 4.7
$0\cup z=\lim(\lambda\varepsilon,-\operatorname{rat}\varepsilon\cup
z)=\lim(\lambda\varepsilon,z)=z$. ∎

We still need to define multiplication, prove that it is continuous and
behaves well regarding $<$, and show that reals apart from $0$ are invertible.

###  4.2 Multiplication

Multiplication is not Lipschitz over all of $\mathbb{Q}$, so we cannot simply
use Lipschitz extension. The definition in HoTT [2013] first defines squaring
and uses the identity $u*v=\frac{(u+v)^{2}-u^{2}-v^{2}}{2}$ to define
multiplication from it. We stay closer to simple Lipschitz extension by
defining multiplication on bounded intervals then joining these to cover .

######  Definition 4.9 (Definition by surjection).

Let $A\;B$ and $C$ sets, and $f:A\rightarrow C$ and $g:A\rightarrow B$
functions such that $g$ is a surjection and $f$ respects $\sim_{g}$ the
equivalence relation on $A$ induced by $g$.

Then $B$ is equivalent to $A/\sim_{g}$ the quotient of $A$ by $\sim_{g}$ and
there is a function $f_{\sim_{g}}:A/\sim_{g}\rightarrow C$ acting like $f$.

Composing $f_{\sim_{g}}$ with the equivalence defines the function
$\overline{f}_{\sim_{g}}:B\rightarrow C$ such that $\forall
x:A,\overline{f}_{\sim_{g}}\;(g\;x)=f\;x$.

######  Definition 4.10 (Intervals).

For $a,b:\mathbb{Q}$ (resp. $a,b:\real$), the interval space
$[a,b]\coloneqq\Sigma_{x}a\leq x\leq b$ inheriting the closeness relation from
the first projection forms a premetric space.

For $x:\mathbb{Q}$ (resp. $x:\real$), $a\leq a\cup(x\cap b)\leq b$ so we can
define $[x]_{a,b}:[a,b]$. If $a\leq x\leq b$ then $[x]_{a,b}$ has its first
projection equal to $x$.

######  Definition 4.11 (Left multiplication by a rational).

For any $q:\mathbb{Q}$, $\lambda r:\mathbb{Q},q*r$ is Lipschitz with constant
$q+1$, so we define $\lambda(q:\mathbb{Q})(y:\real),q*y$ by Lipschitz
extension with constant $a$.

######  Definition 4.12 (Bounded multiplication).

For $a:\mathbb{Q}^{+}$ and $y:[-\operatorname{rat}a,\operatorname{rat}a]$ we
define $\lambda x:\real,x*_{a}y$ by Lipschitz extension.

###### Proof.

We need to check that $\lambda q:\mathbb{Q},q*y$ is Lipschitz with constant
$a$. Using HoTT [2013] theorem 11.3.44 it suffices to show that for $x:\real$
such that $|x|\leq\operatorname{rat}a$ we have $\forall
q\;r:\mathbb{Q},|q*x-r*x|\leq\operatorname{rat}(|q-r|*a)$. This is obtained by
continuity. ∎

######  Lemma 4.13.

Cauchy reals are bounded by rationals, i.e. for all $x:\real$ there merely is
$q:\mathbb{Q}^{+}$ such that $|x|<\operatorname{rat}q$.

###### Proof.

By simple $\operatorname{\mathcal{C}}-$induction on $x$.

In the base case we take $q\coloneqq|x|+1$.

In the limit case, where $x$ is $\lim f$, by the induction hypothesis there
merely is $q:\mathbb{Q}^{+}$ such that $|f\;1|<\operatorname{rat}q$.
$|f\;1|\approx_{2}|x|$ so $x<\operatorname{rat}(q+2)$. ∎

######  Lemma 4.14.

Let the following function be defined by the obvious projections:

$\\{\\_\\}:\Sigma_{a:\mathbb{Q}^{+}}[-\operatorname{rat}a,\operatorname{rat}a]\rightarrow\real$

It is surjective and respects bounded multiplication, i.e.

$\forall x,y,z,\\{x\\}=\\{y\\}\rightarrow z*_{x_{1}}x_{2}=z*_{y_{1}}y_{2}$

###### Proof.

The function is surjective because reals are bounded by rationals. It respects
bounded multiplication by continuity. ∎

######  Definition 4.15 (Multiplication).

For $x:\real$ we define $\lambda y:\real,x*y$ from

$\lambda
y:\Sigma_{a:\mathbb{Q}^{+}}[-\operatorname{rat}a,\operatorname{rat}a],x*_{y_{1}}y_{2}$

and surjectivity of $\\{\\_\\}$.

Multiplication is now defined, with the following properties by definition:

######  Lemma 4.16.

For $x:\real$ and $a:\mathbb{Q}^{+}$ and
$y:[-\operatorname{rat}a,\operatorname{rat}a]$

$x*y_{1}=x*_{a}y$

###### Proof.

By unfolding definition 4.9. ∎

######  Lemma 4.17.

Multiplication computes on rationals:

$\forall
q,r:\mathbb{Q},\operatorname{rat}q*\operatorname{rat}r\equiv\operatorname{rat}(q*r)$

###### Proof.

Checking a conversion is decidable so this proof is left as an exercise to the
reader. ∎

We now need to show that multiplication is continuous as an uncurried
function.

######  Lemma 4.18.

For $a:\mathbb{Q}^{+}$ and $y:\real$ such that $|y|\leq\operatorname{rat}a$,
$\lambda x:\real,x*y$ is Lipschitz with constant $a$.

###### Proof.

Using lemmas 4.16 and 4.12. ∎

######  Lemma 4.19.

For all $y:\real$, $\lambda x:\real,x*y$ is continuous.

###### Proof.

Let $y:\real$, there merely is $a:\mathbb{Q}^{+}$ such that
$|y|\leq\operatorname{rat}a$. By lemma 4.18 $\lambda x:\real,x*y$ is Lipschitz
with constant $a$ and therefore continuous. ∎

######  Lemma 4.20.

For $q:\mathbb{Q}$ and $x:\real$, $\operatorname{rat}q*x=q*x$.

###### Proof.

Using lemma 4.16 for some $a$ bounding $x$. ∎

######  Lemma 4.21.

Multiplication and negation distribute inside the absolute value:

$\forall a,b,c:\real,|a*b-a*c|=|a|*|b-c|$

###### Proof.

We can reduce to the case where $a$ is rational by continuity, then use lemma
4.20 to replace real to real multiplication with rational to real
multiplication and finish by continuity. ∎

######  Lemma 4.22.

Multiplication is compatible with $\leq$ under absolute value: for
$a,b,c,d:\real$, if $|a|\leq|c|$ and $|b|\leq|d|$ then $|a|*|b|\leq|c|*|d|$.

###### Proof.

Again we use continuity to reduce $a$ and $c$ (the variables appearing to the
left of the multiplications) to their rational case, then rewrite the desired
property to use multiplication of a rational and a real and finish with
continuity. ∎

######  Theorem 4.23.

Multiplication is continuous as a function of 2 variables, i.e. given $u_{1}$
and $v_{1}:\real$ and $\varepsilon:\mathbb{Q}^{+}$ there merely exists
$\delta:\mathbb{Q}^{+}$ such that for all $u_{2}$ and $v_{2}:\real$, if
$u_{1}\approx_{\delta}u_{2}$ and $v_{1}\approx_{\delta}v_{2}$ then
$u_{1}*v_{1}\approx_{\varepsilon}u_{2}*v_{2}$.

###### Proof.

Let $u_{1},v_{1}:\real$ and $\varepsilon:\mathbb{Q}^{+}$. There merely is
$\delta:\mathbb{Q}^{+}$ such that $|u_{1}|<\operatorname{rat}\delta$ and
$|v_{1}|<\operatorname{rat}\delta$. Let $\kappa\coloneqq\delta+1$, then in the
lemma’s statement we take $\delta\coloneqq
1\cap\frac{\varepsilon}{2(\kappa+1)}$.

Let $u_{2},v_{2}:\real$ such that

  * •

$u_{1}\approx_{1\cap\frac{\varepsilon}{2(\kappa+1)}}u_{2}$

  * •

$v_{1}\approx_{1\cap\frac{\varepsilon}{2(\kappa+1)}}v_{2}$

Then:

  * •

$u_{1}*v_{1}\approx_{\varepsilon/2}u_{2}*v_{1}$:

$|v_{1}|\leq\operatorname{rat}\delta$ so $\lambda y:\real,y*v_{1}$ is
Lipschitz with constant $\delta$ and it suffices to prove
$u_{1}\approx_{\varepsilon/2\delta}u_{2}$.

This is true from roundedness and the first $\approx$ hypothesis since
$1\cap\frac{\varepsilon}{2(\kappa+1)}\leq\varepsilon/2\delta$.

  * •

$u_{2}*v_{1}\approx_{\varepsilon/2}u_{2}*v_{2}$:

By HoTT [2013] theorem 11.3.44 we look to prove
$|u_{2}*v_{1}-u_{2}*v_{2}|=|u_{2}|*|v_{1}-v_{2}|<\varepsilon/2$.

In fact we have

    * –

$|u_{2}|\leq|\kappa|=\kappa$ since $|u_{1}|\leq\kappa$ and
$u_{1}\approx_{1}u_{2}$.

    * –

$|v_{1}-v_{2}|\leq|\frac{\varepsilon}{2(\kappa+1)}|=\frac{\varepsilon}{2(\kappa+1)}$
since $|v_{1}-v_{2}|<1\cap\frac{\varepsilon}{2(\kappa+1)}$.

Then by lemma 4.22 we have
$|u_{2}|*|v_{1}-v_{2}|\leq|\kappa|*|\frac{\varepsilon}{2(\kappa+1)}|=\varepsilon/2*\frac{\kappa}{\kappa+1}<\varepsilon/2$.

By triangularity $u_{1}*v_{1}\approx_{\varepsilon}u_{2}*v_{2}$. ∎

This is enough to show that forms a partially ordered ring, but we still need
to link multiplication and $<$.

######  Lemma 4.24.

Multiplication of positive values produces a positive value: let $x,y:\real$
such that $0<x$ and $0<y$, then $0<x*y$.

###### Proof.

Let $x,y:\real$ such that $0<x$ and $0<y$, then there merely are
$\varepsilon,\delta:\mathbb{Q}^{+}$ such that $\varepsilon<x$ and $\delta<y$.

By continuity multiplication preserves $\leq$ for nonnegative values, so
$0<\operatorname{rat}(\varepsilon*\delta)\leq x*y$. ∎

######  Lemma 4.25.

For $x,y:\real$, if $0\leq x$ and $0<x*y$ then $0<y$.

###### Proof.

There merely is $\varepsilon:\mathbb{Q}^{+}$ such that
$\operatorname{rat}\varepsilon<x*y$. By lemma 4.13 there merely is
$\delta:\mathbb{Q}^{+}$ such that $|x|<\operatorname{rat}\delta$. Then it
suffices to prove $0<\varepsilon/\delta\leq y$.

We do this using lemma 4.8: suppose $y<\varepsilon/\delta$. Since $0\leq y$
(if $y<0$ then $x*y\leq 0$ which is absurd), $x*y\leq|x|*y\leq\varepsilon<x*y$
which is absurd. ∎

###  4.3 Multiplicative inverse

The multiplicative inverse for $\mathbb{Q}$ is Lipschitz on intervals
$[\varepsilon,+\infty]$ for $\varepsilon:\mathbb{Q}^{+}$. We use this to
extend it to positive reals, then to reals apart from $0$ using negation.

######  Definition 4.26.

For $\varepsilon:\mathbb{Q}^{+}$ the function $\lambda
q:\mathbb{Q},\frac{1}{\varepsilon\cup q}$ is defined and Lipschitz with
constant $\varepsilon^{-2}$.

Then for
$x:\Sigma_{\varepsilon:\mathbb{Q}^{+},x:\real}\operatorname{rat}\varepsilon\leq
x$ we define

$/_{\Sigma}x\coloneqq\left(\overline{\lambda
q:\mathbb{Q},\frac{1}{x_{\varepsilon}\cup q}}\right)x_{x}$

######  Definition 4.27.

We define the inverse of positive reals by surjection (definition 4.9) using
$/_{\Sigma}$ and the obvious surjection from
$x:\Sigma_{\varepsilon:\mathbb{Q}^{+},x:\real}\operatorname{rat}\varepsilon\leq
x$ to $\Sigma_{x:\real}0<x$.

For negative values we use the identity $\frac{1}{x}\coloneqq-\frac{1}{-x}$.

This gives $\frac{1}{x}$ for any $x$ such that $x\operatorname{\\#}0$.

######  Lemma 4.28.

$\forall
q:\mathbb{Q},\operatorname{rat}q\operatorname{\\#}0\rightarrow\frac{1}{\operatorname{rat}q}=\operatorname{rat}(\frac{1}{q})$

###### Proof.

The negative case is easily reduced to the positive case.

In the positive case there merely are $r,s:\mathbb{Q}$ such that $0\leq
r<s\leq q$, then $\frac{1}{\operatorname{rat}q}$ reduces to
$\operatorname{rat}\frac{1}{q\cup s}$ which is equal to
$\operatorname{rat}\frac{1}{q}$ since $s\leq q$. ∎

######  Lemma 4.29.

For $x:\real$ and $\varepsilon:\mathbb{Q}^{+}$ such that
$\operatorname{rat}\varepsilon\leq x$, $\frac{1}{x}=\left(\overline{\lambda
q:\mathbb{Q},\frac{1}{\varepsilon\cup q}}\right)x$.

###### Proof.

Easy. ∎

######  Lemma 4.30.

$\forall x:\real$, if $x\operatorname{\\#}0$ then $x*\frac{1}{x}=1$.

###### Proof.

We can reduce to the case where $0<x$. Then there merely is
$\varepsilon:\mathbb{Q}^{+}$ such that $\operatorname{rat}\varepsilon\leq x$.

By continuity $x*\left(\overline{\lambda q:\mathbb{Q},\frac{1}{\varepsilon\cup
q}}\right)x=1$ for all $x$ such that $\operatorname{rat}\varepsilon\leq x$,
and by definition, $\frac{1}{x}=\left(\overline{\lambda
q:\mathbb{Q},\frac{1}{\varepsilon\cup q}}\right)x$. ∎

Together with the results from HoTT [2013] section 11.3.3 we now have all
results needed for to form an Archimedean ordered field as desired.

##  5 A partial function on Cauchy reals

Without additional axioms, we can’t define any non-constant function from to
booleans $\mathbb{B}$. In other words, no non-trivial property on is
decidable.

However we can encode non-termination as an effect in the _partiality monad_ ,
where the type of computations producing values of type $A$ is denoted
$A_{\bot}$. Then we can define a function $isPositive:\real\rightarrow
2_{\bot}$ which produces $true$ on positive reals, $false$ on negative reals
and does not terminate on $0$.

###  5.1 The partiality monad

In Partiality, Revisited [2016], Altenkirch and Danielsson define the type
$A_{\bot}$ of computations producing values of type $A$ as a HIIT. They
implemented it in Agda and proved certain properties such as the existence of
fixpoints and that it forms the free $\omega-$CPO on $A$.

######  Definition 5.1 (Increasing sequences).

$\operatorname{IncreasingSequence}A\coloneqq\Sigma_{f:\mathbb{N}\rightarrow
A}\forall n,f_{n}\leq f_{Sn}$

As with Cauchy approximations we confuse
$f:\operatorname{IncreasingSequence}A$ with the underlying function in our
notations.

######  Definition 5.2.

Given $A$ a type, the type $A_{\bot}$ is defined simultaneously with its
order. It has the following constructors:

  * •

$\operatorname{\eta}:A\rightarrow A_{\bot}$

  * •

$\bot:A_{\bot}$

  * •

$sup:\operatorname{IncreasingSequence}A_{\bot}\rightarrow A_{\bot}$

with a path constructor of type $\forall x,y:A_{\bot},x\leq y\rightarrow y\leq
x\rightarrow x=y$.

The order has constructors of types

  * •

$\forall x:A_{\bot},x\leq x$

  * •

$\forall x:A_{\bot},\bot\leq x$

  * •

$\forall f,x,sup\;f\leq x\rightarrow\forall n,f_{n}\leq x$

  * •

$\forall f,x,(\forall n,f_{n}\leq x)\rightarrow sup\;f\leq x$

and is truncated to be propositional.

As with the Cauchy completion we have simple induction on values and simple
induction on the auxiliary relation $\leq$ to prove inhabitedness of
propositional types depending on computations, and non-dependent mutual
recursion to define values from computations.

Altenkirch and Danielsson suggest a way of defining
$isPositive:\mathbb{R}^{q}\rightarrow\boldsymbol{2}_{\bot}$, where
$\mathbb{R}^{q}$ is the quotient of Cauchy sequences of $\mathbb{Q}$ by the
appropriate equivalence.

They first define it on Cauchy sequences of $\mathbb{Q}$ using the fixpoint
operator provided by the partiality functor, then show that it respects the
equivalence and extend it to the quotient $\mathbb{R}^{q}$.

We could not adapt that definition for the HIIT Cauchy real numbers. However,
an alternate definition is possible:

  * •

For $P:Prop$,
$\left(\Sigma_{p:\boldsymbol{1}_{\bot}}p=\operatorname{\eta}\star\leftrightarrow
P\right)$ is propositional.

We can use simple $\operatorname{\mathcal{C}}-$induction to define $p$ for all
$P\coloneqq x<\operatorname{rat}q$.

  * •

From $p$ and $q:\boldsymbol{1}_{\bot}$ such that $p$ and $q$ are not both
$\operatorname{\eta}\star$, we define $interleave\;p\;q:\boldsymbol{2}_{\bot}$
indicating which if any is $\operatorname{\eta}\star$.

  * •

We interleave the values defined from $-x<0$ and $x<0$ to define
$isPositive\;x$.

We assume the properties of $A_{\bot}$ for arbitrary $A$ from Partiality,
Revisited [2016]. Let us then focus on the properties of
$\boldsymbol{1}_{\bot}$.

###  5.2 The Sierpinski space

If $A_{\bot}$ is the type of possibly non-terminating computations returning a
value of type $A$, then $\boldsymbol{1}_{\bot}$ is the type of semi-decision
procedures: $p:\boldsymbol{1}_{\bot}$ semi-decides all propositions equivalent
to $p=\operatorname{\eta}\star$.

######  Definition 5.3.

$\boldsymbol{1}_{\bot}$ has a greatest element
$\top\coloneqq\operatorname{\eta}\star$.

###### Proof.

$\forall x:\boldsymbol{1}_{\bot},x\leq\top$ by simple induction on $x$. ∎

We can interpret $p:\boldsymbol{1}_{\bot}$ as the proposition
$p=\operatorname{\eta}\star$ (equivalently, $\operatorname{\eta}\star\leq p$).

Then trivially $\top\leftrightarrow\boldsymbol{1}$,
$\bot\leftrightarrow\boldsymbol{0}$.

######  Lemma 5.4.

For all $a\;b:\boldsymbol{1}_{\bot}$, $a\leq b$ if and only if $a\rightarrow
b$.

###### Proof.

if $a\leq b$ then $a\rightarrow b$: suppose $a$, i.e. $\top\leq a$. Then
$\top\leq a\leq b$, i.e. $b$.

if $a\rightarrow b$ then $a\leq b$: by simple induction on $a$, each case
being trivial. ∎

We can also interpret $\vee$ into $\boldsymbol{1}_{\bot}$ (and $\wedge$, but
we do not need it for $isPositive$).

######  Definition 5.5 (Join on $\boldsymbol{1}_{\bot}$).

###### Proof.

We define an auxiliary function by mutual recursion: for all
$y:\boldsymbol{1}_{\bot}$ there is
$\cup_{y}:\boldsymbol{1}_{\bot}\rightarrow\Sigma_{z:\boldsymbol{1}_{\bot}}y\leq
z$, then $x\cup y\coloneqq(\cup_{y}\;x)_{1}$. Then $x\cup y$ is the first
projection of $\cup_{y}\;x$. It computes as follows:

  * •

$\top\cup\;y\coloneqq\top$

  * •

$\bot\cup\;y\coloneqq y$

  * •

$(\sup f)\cup\;y\coloneqq\sup(\lambda n,f_{n}\cup\;y)$

The proofs of the required properties are trivial. Note that we need the
auxiliary function as we need a proof that $\forall
x:\Sigma_{z:\boldsymbol{1}_{\bot}}y\leq z,\cup_{y}\;\bot=y\leq x_{1}$. ∎

######  Lemma 5.6.

$x\cup y$ is the least upper bound of $x$ and $y$. Then $\cup$ is a monoid
operator with identity element $\bot$.

###### Proof.

By definition and simple inductions. ∎

######  Lemma 5.7.

For all $a\;b:\boldsymbol{1}_{\bot}$, $a\cup b$ if and only if $a\vee b$.

###### Proof.

If $a\vee b$ then trivially $a\cup b$, $a\cup b$ being an upper bound of $a$
and $b$.

The other direction is obtained by simple induction on $a$. ∎

$\boldsymbol{1}_{\bot}$ has a countable join operator, but it is limited to
increasing sequences. Thanks to the binary join we can remove this limit to
define interpret properties $\exists n:\mathbb{N},P_{n}$ and even $\exists
x:A,P\;x$ when $A$ is enumerable.

######  Definition 5.8.

For all $f:\mathbb{N}\rightarrow\boldsymbol{1}_{\bot}$ there is a least upper
bound $\sup f$ of all the $f_{n}$.

###### Proof.

We have $\sup f$ for monotonous sequences, so for arbitrary
$f:\mathbb{N}\rightarrow\boldsymbol{1}_{\bot}$ we define
$f^{\leq}:\mathbb{N}\rightarrow\boldsymbol{1}_{\bot}$ by
$f^{\leq}\;n\coloneqq\bigcup_{m\leq n}f\;m$.

Then $f^{\leq}$ is monotonous and $\sup f\coloneqq\sup f^{\leq}$ is the least
upper bound of all the $f_{n}$. ∎

That $\sup f$ semi-decides $\exists x,f\;x$ is trivial.

###  5.3 Interleaving

######  Definition 5.9 (Disjoint).

$a$ and $b:\boldsymbol{1}_{\bot}$ are disjoint when they do not both hold,
i.e. $a\rightarrow b\rightarrow\boldsymbol{0}$.

Interleaving lets us define a value in $\boldsymbol{2}_{\bot}$ from two values
in $\boldsymbol{1}_{\bot}$ which are not both $\top$. If we see
$x\;y:\boldsymbol{1}_{\bot}$ as semi-decision procedures then the interleaving
of $x$ and $y$ is $\operatorname{\eta}true$ if $x$ terminates (i.e. $x=\top$),
$false$ if $y$ terminates and does not terminate if neither terminates. If
computing on a Turing machine it would be obtained by interleaving simulated
steps of $x$ and $y$ until one terminates, then returning a value depending on
which one terminated.

We can only interleave disjoint values: a Turing machine could pick whichever
one terminates first, but we have hidden those distinctions away using higher
inductive types.

######  Definition 5.10.

We define by mutual induction a function

$\begin{split}interleave\star:\forall
a\;b:\boldsymbol{1}_{\bot},disjoint\;a\;b\rightarrow\\\
\Sigma_{c:\boldsymbol{1}_{\bot}}(map\;(\lambda\\_,false)\;b)\leq
c)\end{split}$

where $map:\forall A\;B:Type,(A\rightarrow B)\rightarrow A_{\bot}\rightarrow
B_{\bot}$ is the map of the partiality monad, and in parallel a proof that for
all $a\;a^{\prime}:\boldsymbol{1}_{\bot}$, if $a\leq a^{\prime}$ then for all
$b:\boldsymbol{1}_{\bot}$ disjoint with $a$ and with $a^{\prime}$,
$interleave_{\star}\;a\;b\leq interleave_{\star}\;a^{\prime}\;b$.

Then the interleaving function $interleave$ is the first projection of
$interleave_{\star}$. It computes as follows:

  * •

$interleave\;\top\;b\coloneqq\operatorname{\eta}true$

  * •

$interleave\;\bot\;b\coloneqq map\;(\lambda\\_,false)b$

  * •

$interleave\;(\sup f)\;b\coloneqq\sup(\lambda n,interleave\;f_{n}\;b$

Some attention must be taken to keep track of the disjointness proofs which
are left implicit on paper.

######  Lemma 5.11.

If $a:\boldsymbol{1}_{\bot}$ is disjoint from $\top$ then

$interleave\;a\;\top=\operatorname{\eta}false$

###### Proof.

$a$ is disjoint from $\top$ so $a=\bot$ and
$interleave\;a\;\top=map\;(\lambda\\_,false)\;\top=\operatorname{\eta}false$.
∎

######  Lemma 5.12.

For $a\;b:\boldsymbol{1}_{\bot}$ disjoint
$interleave\;a\;b=\operatorname{\eta}true$ (resp. $\operatorname{\eta}false$)
if and only if $a$ holds (resp. $b$ holds).

###### Proof.

By simple induction on $a$ in the first direction, by computation in the
second (note that if $b$ then $a=\bot$ as they are disjoint). ∎

###  5.4 Partial comparison of real numbers with rational numbers

######  Lemma 5.13.

For all $x:\real$ and $q:\mathbb{Q}$, $x<\operatorname{rat}q$ is semi-
decidable, i.e. $\exists s:\boldsymbol{1}_{\bot},s\leftrightarrow
x<\operatorname{rat}q$.

###### Proof.

By simple induction on $x$.

In the base case, for all $q\;r:\mathbb{Q}$,
$\operatorname{rat}q<\operatorname{rat}r$ is decidable so we pick
$s\coloneqq\top$ or $\bot$ as appropriate.

In the limit case, if $x:\operatorname{Approximation}\real$ such that for all
$\varepsilon$ and $q$, $x_{\varepsilon}<\operatorname{rat}q$ is semi-
decidable, let $q:\mathbb{Q}$, we take
$s\coloneqq\exists\varepsilon\;\delta:\mathbb{Q}^{+},x_{\varepsilon}<\operatorname{rat}(q-\varepsilon-\delta)$
(interpreted as a value in $\boldsymbol{1}_{\bot}$). Then to show correctness:

  * •

if
$\exists\varepsilon\;\delta:\mathbb{Q}^{+},x_{\varepsilon}<\operatorname{rat}(q-\varepsilon-\delta)$
then $\lim
x<\operatorname{rat}q=\operatorname{rat}(q-\varepsilon-\delta+\varepsilon+\delta)$
by lemma 4.3.

  * •

if $\lim x<\operatorname{rat}q$, there merely is $r:\mathbb{Q}$ such that
$\lim x<\operatorname{rat}r$ and $r<q$. Let $\varepsilon\coloneqq q-r$.
Then
$x_{\frac{\varepsilon}{4}}<\operatorname{rat}(q-\varepsilon-\varepsilon)=\operatorname{rat}(r+\varepsilon+\varepsilon)$
by lemma 4.3.

∎

######  Definition 5.14.

For $x:\real$ let $isPositive\;x$ be the interleaving of the semi-decisions
for $-x<0$ and $x<0$.

######  Theorem 5.15.

Let $x:\real$.

  * •

$0<x$ if and only if $isPositive\;x=\operatorname{\eta}true$

  * •

$x<0$ if and only if $isPositive\;x=\operatorname{\eta}false$

  * •

$isPositive\;0=\bot$

###### Proof.

By lemmas 5.11 and 5.12 and computation. ∎

##  6 Conclusion

We have defined a Cauchy completion operation which is a monad on the category
of spaces with an appropriate closeness relation and Lipschitz functions. When
applied to the space of rational numbers it produces a Cauchy complete
archimedean ordered field generated by rationals and limits of Cauchy
approximations, i.e. the Cauchy reals. Finally we have defined and proven
correct a semi-decision procedure (in the sense of Partiality, Revisited
[2016]) for comparing a Cauchy real and a rational number.

## Acknowledgements

This paper is the result of two internships under the direction of Bas
Spitters, at Radbough University and at the University of Aarhus.

## References

  *   * HoTT [2013] The Univalent Foundations Program, Institute for Advanced Study _Homotopy Type Theory: Univalent Foundations of Mathematics_ http://homotopytypetheory.org/book/
  * MathClasses [2011] Bas Spitters and Eelis van der Weegen _Type Classes for Mathematics in Type Theory_ https://math-classes.github.io/
  * Partiality, Revisited [2016] Thorsten Altenkirch, Nils Anders Danielsson _Partiality, Revisited_ TYPES 2016
  * OConnor07 [2007] Russell O’Connor _A Monadic, Functional Implementation of Real Numbers_ Mathematical Structures in Computer Science 17(1): 129-159 (2007)