The HoTT reals coincide with the Escard\'o-Simpson reals

TL;DR

This paper proves that the HoTT reals and the Escardó-Simpson reals are equivalent in the category of sets, establishing their universal property and their characterization as the least Cauchy complete subset of Dedekind reals containing the rationals.

Contribution

It demonstrates the equivalence of HoTT reals and Escardó-Simpson reals and characterizes the HoTT reals as the minimal Cauchy complete subset of Dedekind reals.

Findings

HoTT reals satisfy the universal property of the interval object.

The HoTT reals coincide with the least Cauchy complete subset of Dedekind reals.

The equivalence holds in the category of sets of any universe.

Abstract

Escard\'o and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher-inductive notion of reals, and suggests that the interval may satisfy this universal property. We show that this is indeed the case in the category of sets of any universe. We also show that the type of HoTT reals is the least Cauchy complete subset of the Dedekind reals containing the rationals.

Equations

$$\prod _{a:A}\mathsf{isProp}\left(\sum _{c:C}fc=a\right)$$

$$\prod _{c,c^{\prime }:C}\mathsf{isEquiv}({\mathsf{ap}}_{f,c,c^{\prime }})$$

$$P\subseteq Q:=\forall (a:A).(a\in P)\to (a\in Q),$$

$$\left(\bigcup E\right)(a):=\exists (P:A\to \Omega ).(P\in E)\times (a\in P),$$

$$\left(\bigcap E\right)(a):=\forall (P:A\to \Omega ).(P\in E)\to (a\in P).$$

$$\mathbf{Q}:=(\mathbf{Z}\times \mathbf{N})/\sim$$

$${\mathbf{Q}}_{+}:=\left\{q:\mathbf{Q}\mid q>0\right\}=\sum _{q:\mathbf{Q}}(q>0).$$

$$\cdot {\sim }_{\cdot }\cdot :{\mathbf{Q}}_{+}\times R\times R\to \Omega .$$

$$\mathrm{isCauchy}(x):=\forall (\delta ,\epsilon :{\mathbf{Q}}_{+}).x_{\delta }{\sim }_{\delta +\epsilon }{x}_{\epsilon }.$$

$${\mathcal{C}}_R:=\sum _{x:{\mathbf{Q}}_{+}\to R}\mathrm{isCauchy}(x).$$

$$\forall (\epsilon ,\theta :{\mathbf{Q}}_{+}).x_{\epsilon }{\sim }_{\epsilon +\theta }u.$$

$$\mathrm{rat}:$$

$$\lim :$$

$$\mathrm{eq}:$$

$$\prod _{q,r:\mathbf{Q}}\prod _{\epsilon :{\mathbf{Q}}_{+}}(-\epsilon <q-r<\epsilon )\to \mathrm{rat}(q){\sim }_{\epsilon }\mathrm{rat}(r)$$

$$\prod _{q:\mathbf{Q}}\prod _{y:{\mathcal{C}}_R}\prod _{\epsilon ,\delta :{\mathbf{Q}}_{+}}\mathrm{rat}(q){\sim }_{\epsilon }{y}_{\delta }\to \mathrm{rat}(q){\sim }_{\epsilon +\delta }\lim (y)$$

$$\prod _{x:{\mathcal{C}}_R}\prod _{r:\mathbf{Q}}\prod _{\epsilon ,\delta :{\mathbf{Q}}_{+}}{x}_{\delta }{\sim }_{\epsilon }\mathrm{rat}(r)\to \lim (x){\sim }_{\epsilon +\delta }\mathrm{rat}(r)$$

$$\prod _{x:{\mathcal{C}}_R}\prod _{y:{\mathcal{C}}_R}\prod _{\epsilon ,\delta ,\eta :{\mathbf{Q}}_{+}}{x}_{\delta }{\sim }_{\epsilon }{y}_{\eta }\to \lim (x){\sim }_{\epsilon +\delta +\eta }\lim (y)$$

$$\mathsf{CS}-\mathsf{hom}(R,S):=$$

$$\left(\prod _{q:\mathbf{Q}}f(\mathrm{rat}(q))=\mathrm{rat}(q)\right)\times \left(\prod _{x:{\mathcal{C}}_R}f(\lim (x))=\lim (x)\right)$$

$$\times \left(\prod _{u,v:R}\prod _{p:\forall (\epsilon :{\mathbf{Q}}_{+}).u{\sim }_{\epsilon }v}{f}^{\ast }(\mathrm{eq}(u,v,p))=\mathrm{eq}(u,v,p)\right).$$

$$A$$

$$B$$

$$(u,a){\sim }_{\epsilon }(v,b):=\sum _{\zeta :u{\sim }_{\epsilon }v}B(u,v,a,b,\epsilon ,\zeta )$$

$$\forall (\delta ,\epsilon :{\mathbf{Q}}_{+}).a_{\delta }{\sim }_{\delta +\epsilon }{a}_{\epsilon }.$$

$$\lambda \epsilon .(x_{\epsilon },a_{\epsilon })$$

$$f_{\mathrm{rat}}:$$

$$f_{\lim }:$$

$$f_{\mathrm{eq}}:$$

$$\prod _{q,r:\mathbf{Q}}\prod _{\epsilon :{\mathbf{Q}}_{+}}-\epsilon <q-r<\epsilon \to f_{\mathrm{rat}}(q){\sim }_{\epsilon }{f}_{\mathrm{rat}}(r)$$

$$\prod _{q:\mathbf{Q}}\prod _{y:{\mathcal{C}}_{{\mathbf{R}}_{\mathbf{C}}}}\prod _{b:{\mathcal{D}}_A^y}\prod _{\delta ,\epsilon :{\mathbf{Q}}_{+}}\mathrm{rat}(q){\sim }_{\epsilon }{y}_{\delta }$$

$$\to f_{\mathrm{rat}}(q){\sim }_{\epsilon }{b}_{\delta }\to f_{\mathrm{rat}}(q){\sim }_{\epsilon +\delta }{f}_{\lim }(y,b)$$

$$\prod _{x:{\mathcal{C}}_{{\mathbf{R}}_{\mathbf{C}}}}\prod _{a:{\mathcal{D}}_A^x}\prod _{r:\mathbf{Q}}\prod _{\delta ,\epsilon :{\mathbf{Q}}_{+}}{x}_{\delta }{\sim }_{\epsilon }\mathrm{rat}(r)$$

$$\to a_{\delta }{\sim }_{\epsilon }{f}_{\mathrm{rat}}(r)\to f_{\lim }(x,a){\sim }_{\epsilon +\delta }{f}_{\mathrm{rat}}(r)$$

$$\prod _{x,y:{\mathcal{C}}_{{\mathbf{R}}_{\mathbf{C}}}}\prod _{a:{\mathcal{D}}_A^x}\prod _{b:{\mathcal{D}}_A^y}\prod _{\delta ,\eta ,\epsilon :{\mathbf{Q}}_{+}}{x}_{\delta }{\sim }_{\epsilon }{y}_{\eta }$$

$$\to a_{\delta }{\sim }_{\epsilon }{b}_{\eta }\to f_{\lim }(x,a){\sim }_{\epsilon +\delta +\eta }{f}_{\lim }(y,b)$$

$$f:$$

$$g:$$

$$f(\mathrm{rat}(q))$$

$$f(\lim (x))$$

$$(f,g){[x]}_{\epsilon }:=f(x_{\epsilon }).$$

Full text

1 Introduction

Escardó and Simpson defined a notion of interval object by a universal property in any category with binary products, so that in some categories of interest, one gets the intended object [2]. For example, in the category of sets, the interval object exists and its carrier is any real interval $[a,b]$, with $a<b$, in the category of topological spaces it is this interval with its usual Hausdorff topology, and in an elementary topos it is the subobject of the Dedekind reals discussed in Section 2.6 below. Vickers also showed that in the category of locales, it is the usual compact interval locale, a regular subobject of the locale of real numbers [13].

Independently of this, the HoTT book [12, Section 11.3] introduced a higher-inductive notion of reals that we refer to as the HoTT reals. They are specified as a higher inductive-inductive type: namely a family of types that is defined mutually by both constructors of those types, and constructors of their identity types. It is a Cauchy-style construction, but is in fact Cauchy complete, whereas in general the Cauchy reals are not [5].

Our contribution is to show that, in univalent type theory, the interval in the HoTT reals ${\mathbf{R}_{\mathbf{C}}}$ is an interval object. We establish this by showing that the HoTT reals are equivalent to a certain subset ${\mathbf{R}_{\mathbf{E}}}$ of the Dedekind reals ${\mathbf{R}_{\mathbf{D}}}$. Then we use the proof of Escardó and Simpson that the interval in ${\mathbf{R}_{\mathbf{E}}}$ is an interval object. This answers a question left open in the HoTT book [12, Notes for Chapter 11] and on the nLab [6].

In order to use the above proof by Escardó and Simpson, we translate topos-theoretical proofs to univalent type theory. Specifically, to get a subobject classifier we use propositional resizing [14, 15]. However, the proof that the HoTT reals are equivalent to a subset of ${\mathbf{R}_{\mathbf{D}}}$ also works in a predicative setting. It may be possible to show directly that the interval in the HoTT reals is an interval object, without going via ${\mathbf{R}_{\mathbf{E}}}$, and this may result in a proof that works in a predicative setting. This will be the topic of further work.

2 Preliminaries

We write $\mathcal{U}$ for a univalent universe. We treat the hierarchy of universes as cumulative. Given a type $X$, we write $\|X\|$ for its propositional truncation. By “there exists $a:A$ such that $B(a)$” we mean $(\exists(a:A).B(a))\coloneqq\left\|\sum_{a:A}B(a)\right\|$, and by the disjunction $X\vee Y$ we mean $\|X+Y\|$. An equivalence $e:X\simeq Y$ between two types $X$ and $Y$ is given by a map $f:X\to Y$ which has both a left inverse and a right inverse, and we conflate equivalences $X\simeq Y$ with their underlying map $X\to Y$. We write $\Omega$ for the type of propositions.

2.1 Subtypes and embeddings

Definition 1**.**

By a subtype of $A:\mathcal{U}$ we mean a map $B:A\to\Omega$. For $a:A$ we define $(a\in B)\coloneqq B(a)$.

This is motivated by the fact that if $B:A\to\Omega$ is a a subtype of $A$, then the projection map $\operatorname{\mathsf{p}}_{0}:\sum_{a:A}B(a)\to A$ is an embedding, and vice versa embeddings give rise to subtypes, as we will make precise in Lemma 3.

Definition 2**.**

Given a function $f:C\to A$, we say $f$ is an embedding, and write $f:C\hookrightarrow A$, if one of these two equivalent conditions holds:

[TABLE]

The second condition expresses that $\mathsf{ap}_{f,c,c^{\prime}}:(c=_{C}c^{\prime})\to(fc=_{A}fc^{\prime})$ is an equivalence for all $c,c^{\prime}:C$.

The above two notions are equivalent:

Lemma 3**.**

Subtypes $B:A\to\Omega$ of $A$ correspond to types $C$ that embed into $A$.

Proof.

In one direction, the type $C\coloneqq\sum_{a:A}B(a)$ embeds into $A$ by the projection map. Conversely, given an embedding $f:C\hookrightarrow A$, the subtype is given by $B(a)\coloneqq\sum_{c:C}(fc=a)$, which is well-defined by the fact that $f$ is an embedding. For details, see e.g. Rijke et al. [9, Theorem 2.29]. ∎

We will use this correspondence implicitly.

Lemma 4**.**

Subtypes of $A$ form a poset by defining, for $P:A\to\Omega$ and $Q:A\to\Omega$:

[TABLE]

where $(P\subseteq Q):\Omega$. Explicitly, with additionally $R:A\to\Omega$:

$P\subseteq P$, 2. 2.

$(P\subseteq Q)\to(Q\subseteq P)\to P=Q$, 3. 3.

$(P\subseteq Q)\to(Q\subseteq R)\to(P\subseteq R)$.

Proof.

Straightforward. ∎

Our main contribution uses the following formulation of the second law of Lemma 4, which we prove more explicitly. Note that for embeddings from $C$ and $D$ into $A$, the relation $C\subseteq D$ holds if we have a commutative triangle.

Lemma 5**.**

Suppose given a triangle of maps as follows.

{C}$${D}$${\bigcirc}$${A}$$\scriptstyle{g}$$\scriptstyle{i_{C}}$$\scriptstyle{f}$$\scriptstyle{i_{D}}

If $i_{C}$ and $i_{D}$ are embeddings, and the commutativity conditions $i_{C}\circ f=i_{D}$ and $i_{D}\circ g=i_{C}$ are satisfied, then $f$ and $g$ are equivalences.

Proof.

It suffices to show that $g\circ f={\mathsf{id}_{D}}$ and $f\circ g={\mathsf{id}_{C}}$.

By the fact that $i_{C}$ and $i_{D}$ are embeddings, and using function extensionality, this is equivalent to showing that $i_{D}\circ g\circ f=i_{D}$ and $i_{C}\circ f\circ g=i_{C}$. Both cases can be shown by applying commutativity of the triangle both ways round. Explicitly, $i_{D}\circ g\circ f=i_{C}\circ f=i_{D}$ and $i_{C}\circ f\circ g=i_{D}\circ g=i_{C}$. ∎

In fact, the horizontal maps are automatically embeddings, but we will not use this.

Lemma 6**.**

The poset of subtypes of $A$ is closed under joins and meets of a subtype $E:(A\to\Omega)\to\Omega$ of the type of subtypes of $A$. In other words, for any $E:(A\to\Omega)\to\Omega$ the join $\bigcup E$ and meet $\bigcap E$ exist.

Proof.

The join $\bigcup E:A\to\Omega$ is given by

[TABLE]

and its meet by

[TABLE]

For the join, we need to prove that if $P\in E$ then $P\subseteq\bigcup E$, and that if $Q:A\to\Omega$ has $P\subseteq Q$ for any $P\in E$, then $\bigcup E\subseteq Q$.

For the former, let $P\in E$ and $a\in P$. We need to show $\exists(P:A\to\Omega).(P\in E)\times(a\in P)$. But the $P$ we started with is such.

For the latter, suppose $P\subseteq Q$ for all $P\in E$, and suppose there exists $P^{\prime}\in E$ with $a\in P^{\prime}$. Then we need to show that $a\in Q$. But this is true since $P^{\prime}\subseteq Q$.

The proof for the meet is similar. ∎

2.2 Rationals

Let $\mathbf{N}$ and $\mathbf{Z}$ be appropriate types of naturals and integers. We define a type of rationals, for example, as the quotient type

[TABLE]

where a pair $(d,n)$ represents the rational $\frac{d}{n+1}$ and $\sim$ is an appropriate equivalence relation. Constructions without quotient types are also possible as the rationals can be enumerated without repetition. It will be convenient to additionally define the type of positive rationals:

[TABLE]

2.3 Cauchy structures

Following Sojakova [10], we take an algebraic view on types of real numbers, as well as on HIITs. By analogy with Richman [8], we define premetric spaces. By analogy with the HoTT book [12], we define $\varepsilon$-closeness.

Definition 7**.**

A premetric on a type $R:\mathcal{U}$ is a relation

[TABLE]

We will often write $R$ for the premetric space $(R,\sim)$, leaving the premetric $\sim$ implicit. In the case that $u\sim_{\varepsilon}v$ holds (where $\varepsilon:\mathbf{Q}_{+}$ and $u,v:R$) we say that $u$ and $v$ are $\varepsilon$-close.

Definition 8**.**

If $R$ is a premetric space, then $x:\mathbf{Q}_{+}\to R$ is a Cauchy approximation if

[TABLE]

We define the type $\mathcal{C}_{R}$ of Cauchy approximations in $R$ as

[TABLE]

Since being a Cauchy approximation is a property rather than structure, we conflate elements of $\mathcal{C}_{R}$ with their underlying map $\mathbf{Q}_{+}\to R$.

Definition 9**.**

If $x$ is a Cauchy approximation in a premetric space $R$, then we say that $u:R$ is a limit of $x$ if

[TABLE]

If every Cauchy approximation has a limit, we say that $R$ is Cauchy complete.

Definition 10**.**

A Cauchy structure is a premetric space $R$ together with the following structure.

[TABLE]

A morphism of Cauchy structures from $R$ to $S$ is a map $f:R\to S$ and a family of maps $g_{\varepsilon,u,v}:u\sim_{\varepsilon}v\to f(u)\sim_{\varepsilon}f(v)$ that preserve $\operatorname{\mathsf{rat}}$, $\operatorname{\mathsf{lim}}$ and $\operatorname{\mathsf{eq}}$ in the obvious sense. Explicitly:

[TABLE]

Remark*.*

The remaining four maps of the Cauchy structure are automatically preserved as $\sim$ is valued in propositions. 2. 2.

A morphism of Cauchy structures from $R$ to $S$ gives rise to a map $\mathcal{C}_{R}\to\mathcal{C}_{S}$. 3. 3.

Identity maps are Cauchy structure morphisms, and Cauchy structure morphisms are closed under composition. 4. 4.

We emphasize that even though a Cauchy structure has the $\operatorname{\mathsf{lim}}$ map, it need not be Cauchy complete, since the elements $x_{\varepsilon}$ of a Cauchy approximation might not be of the form $\operatorname{\mathsf{rat}}(q)$ or $\operatorname{\mathsf{lim}}(z)$. In other words, the $\operatorname{\mathsf{lim}}$ map does not necessarily compute limits.

2.4 HoTT reals

We now define the HoTT reals ${\mathbf{R}_{\mathbf{C}}}$ [12, Section 11.3]. We use the following definition, which is equivalent to the one in the HoTT book by Theorem 17.

Definition 11**.**

${\mathbf{R}_{\mathbf{C}}}$ is a homotopy-initial Cauchy structure, in the sense that for any other Cauchy structure $S$, the type of Cauchy structure morphisms from ${\mathbf{R}_{\mathbf{C}}}$ to $S$ is contractible.

Theorem 12**.**

${\mathbf{R}_{\mathbf{C}}}$* is Cauchy complete.*

To prove this theorem, we will develop an induction principle for ${\mathbf{R}_{\mathbf{C}}}$.

Definition 13**.**

Given

[TABLE]

we obtain a natural premetric on $\sum_{u:{\mathbf{R}_{\mathbf{C}}}}A(u)$, given by the relation:

[TABLE]

For the remainder of this section, fix a choice of $A:{\mathbf{R}_{\mathbf{C}}}\to\mathcal{U}$ and $B:\prod_{u,v:{\mathbf{R}_{\mathbf{C}}}}A(u)\to A(v)\to\prod_{\varepsilon:\mathbf{Q}_{+}}(u\sim_{\varepsilon}v)\to\Omega$ — these type families will be input for our induction principle. The remaining input will allow us to define a Cauchy structure on $\sum_{u:{\mathbf{R}_{\mathbf{C}}}}A(u)$. We will often denote the type $B(u,v,a,b,\varepsilon,\zeta)$ by $a\sim_{\varepsilon}b$, since $u$ can typically be inferred from $a$ and $v$ from $b$, and $\zeta$ is unique since the premetric on ${\mathbf{R}_{\mathbf{C}}}$ is valued in propositions.

Definition 14**.**

Let $x:\mathcal{C}_{{\mathbf{R}_{\mathbf{C}}}}$ and $a:\prod_{\varepsilon:\mathbf{Q}_{+}}A(x_{\varepsilon})$, satisfying

[TABLE]

Then we call $a$ a dependent Cauchy approximation over $x$. We denote the type of all dependent Cauchy approximations over $x$ by $\mathcal{D}_{A}^{x}$, and again conflate its elements with their underlying (dependent) function.

Lemma 15**.**

Suppose $x:\mathcal{C}_{{\mathbf{R}_{\mathbf{C}}}}$ and $a:\prod_{\varepsilon:\mathbf{Q}_{+}}A(x_{\varepsilon})$. Then the function

[TABLE]

is a Cauchy approximation in $\sum_{u:{\mathbf{R}_{\mathbf{C}}}}A(u)$ iff $a$ is a dependent Cauchy approximation over $x$.

Proof.

Straightforward. ∎

The above lemma allows us to take limits componentwise, as we will do in the proof of an induction principle in Theorem 17. To be able to phrase an induction principle, we need to be able to talk about dependent paths: namely the equality of elements in fibers over equal elements of ${\mathbf{R}_{\mathbf{C}}}$.

Definition 16**.**

Given a type $A:\mathcal{U}$, a type family $B:A\to\mathcal{U}$, a path $p:x=_{A}y$ in $A$, and elements $u:B(x)$ and $v:B(y)$, the type of dependent paths $u=_{p}^{B}v$ is defined by induction on $p$: if $p$ is $\operatorname{\mathsf{refl}}(x)$ then $(u=_{\operatorname{\mathsf{refl}}(x)}^{B}v)\coloneqq(u=_{B(x)}v)$. We refer to elements of $u=_{p}^{B}v$ as paths from $u$ to $v$ over $p$.

In particular, a path $p:x=_{A}y$ can be combined with a dependent path $q:u=_{p}^{B}v$ into a path $(x,u)=_{\sum_{a:A}B(a)}(y,v)$ in the dependent sum type, and vice versa a path in the dependent sum type gives rise to a path $p$ in $A$ and a path over $p$.

Theorem 17**.**

Suppose we are provided the following data.

[TABLE]

In that case, we obtain

[TABLE]

satisfying

[TABLE]

where $(f,g)[x]$ is the dependent Cauchy approximation defined by

[TABLE]

Proof.

We reason similar to Sojakova [10]. Write $T=\sum_{u:{\mathbf{R}_{\mathbf{C}}}}A(u)$. Given the input data, we can define a natural Cauchy structure on $T$. For example, $\operatorname{\mathsf{rat}}_{T}(q)\coloneqq(\operatorname{\mathsf{rat}}(q),f_{\operatorname{\mathsf{rat}}}(q))$.

Hence, by homotopy-initiality of ${\mathbf{R}_{\mathbf{C}}}$, we obtain $h:{\mathbf{R}_{\mathbf{C}}}\to T$ and $i_{\varepsilon,u,v}:u\sim_{\varepsilon}v\to h(u)\sim_{\varepsilon}h(v)$ preserving $\operatorname{\mathsf{rat}}$, $\operatorname{\mathsf{lim}}$ and $\operatorname{\mathsf{eq}}$ in the obvious sense.

Postcomposing $h$ and $i$ (the latter componentwise) with the first projection functions gives us a Cauchy morphism ${\mathbf{R}_{\mathbf{C}}}\to{\mathbf{R}_{\mathbf{C}}}$, and so by homotopy-initiality, the first component of any $h(u)$ is equal to $u$. So by transport, we obtain dependent functions $f$ and $g$ with the required properties. ∎

We now appeal to the HoTT book [12, Section 11.3.2] for a proof of Theorem 12.

2.5 Dedekind reals

We will define the Dedekind cuts as a pairs $x=(L,U)$ of predicates $L:\mathbf{Q}\to\Omega$ and $U:\mathbf{Q}\to\Omega$. The following notation will help. Let $q,r:\mathbf{Q}$ and $x=(L,U)$ a pair of predicates, then we write

[TABLE]

We are thus overloading the inequality relation $<$ since it was already defined as a relation on $\mathbf{Q}$.

Definition 18**.**

$x=(L,U)$ is a Dedekind cut if it satisfies the following conditions.

inhabited: $\exists(q:\mathbf{Q}).q<x$ and $\exists(r:Q).x<r$. 2. 2.

rounded: For all $q:\mathbf{Q}$,

[TABLE] 3. 3.

transitivity: $(q<x)\land(x<r)\Rightarrow(q<r)$ for all $q:\mathbf{Q}$. 4. 4.

located: $(q<r)\Rightarrow(q<x)\lor(x<r)$ for all $q,r:\mathbf{Q}$.

We let $\operatorname{isCut}(L,U)$ denote the conjunction of these conditions. The type of Dedekind reals is

[TABLE]

Remark*.*

In the presence of the roundedness axiom, by trichotomy of the rationals, transitivity is equivalent to the disjointness axiom, which states that for all $q:\mathbf{Q}$ we have $\neg(q<x\land x<q)$.

Dedekind reals can be approximated by rationals. The following proof is based on Troelstra and van Dalen [11, Proposition 5.5.2].

Lemma 19**.**

For any $x:{\mathbf{R}_{\mathbf{D}}}$ and $n:\mathbf{N}$ there exist $s,t:\mathbf{Q}$ such that $s<x$ and $x<t$ and $t-s<2^{-n}$.

Proof.

By inhabitedness, there exist $q,r:\mathbf{Q}$ such that $q<x$ and $x<r$. Since we want to show a proposition, we may assume that we have such $q$ and $r$. Choose $m:\mathbf{N}$ and $q_{i}:\mathbf{Q}$ such that $q=q_{0}<q_{1}<\cdots<q_{m+1}=r$ and $q_{i+1}-q_{i}<2^{-n-1}$. By locatedness, for all $0\leq i\leq m$, we have $(q_{i}<x)\vee(x<q_{i+1})$. Suppose instead that we have $\prod_{0\leq i\leq m}(q_{i}<x)+(x<q_{i+1})$ (that is, ignore the truncation around the disjunction for now). In that case, we pick the first $i$ that yields $x<q_{i+1}$, if it exists. If it does not exist, that means $q_{m}<x$, so we set $s\coloneqq q_{m}$ and $t\coloneqq q_{m+1}$. If $i$ exists and is 0, we set $s\coloneqq q_{0}$ and $t\coloneqq q_{1}$. If $i$ exists and is greater than 0, we set $s\coloneqq q_{i-1}$ and $t\coloneqq q_{i+1}$. By functoriality of truncation, this argument tells us that if $\left\|\prod_{0\leq i\leq m}(q_{i}<x)+(x<q_{i+1})\right\|$, then there exist $s$ and $t$ as required. Since truncation distributes over finite products, we are done. ∎

We will now endow ${\mathbf{R}_{\mathbf{D}}}$ with a Cauchy structure. We define the embedding of the rationals, addition, subtraction, the inequality relation, the absolute value function, and the premetric on ${\mathbf{R}_{\mathbf{D}}}$, for $q,r:\mathbf{Q}$ and $x,y:{\mathbf{R}_{\mathbf{D}}}$ and $\varepsilon:\mathbf{Q}_{+}$:

[TABLE]

Theorem 20**.**

${\mathbf{R}_{\mathbf{D}}}$* is Cauchy complete.*

Proof.

Let $x:\mathcal{C}_{\mathbf{R}_{\mathbf{D}}}$. We define $\operatorname{\mathsf{lim}}(x):{\mathbf{R}_{\mathbf{D}}}$ by:

[TABLE]

The details of well-definedness of the map $\operatorname{\mathsf{lim}}$, as well as a proof that it constructs limits, can be found in the HoTT book [12, Theorem 11.2.12]. ∎

Theorem 21**.**

${\mathbf{R}_{\mathbf{D}}}$* and the previously constructed $\operatorname{\mathsf{rat}}$ and $\operatorname{\mathsf{lim}}$ can be completed to obtain a Cauchy structure.*

For this we will use the following.

Lemma 22**.**

For $x:\mathcal{C}_{\mathbf{R}_{\mathbf{D}}}$ and $u:{\mathbf{R}_{\mathbf{D}}}$, we have $\operatorname{\mathsf{lim}}(x+u)=\operatorname{\mathsf{lim}}(x)+u$, where $x+u$ is the Cauchy approximation given by $\lambda\varepsilon.x_{\varepsilon}+u$.

Proof.

One can show, for example by first showing that the Dedekind reals form a group, that $x+u$ is a Cauchy approximation. The remainder is straightforward by unrolling the definitions. ∎

Proof of Theorem 21.

The remaining ingredients are $\operatorname{\mathsf{eq}}$ and verification of the four distance laws.

First, $\operatorname{\mathsf{eq}}$. Suppose that $u$ and $v$ are $\varepsilon$-close for arbitrary $\varepsilon:\mathbf{Q}_{+}$. We need to show that $u=v$. Without loss of generality, we show that for $q:\mathbf{Q}$, if $q<u$ then $q<v$. By roundedness, there exists $q^{\prime}:\mathbf{Q}$ with $q<q^{\prime}<u$. By locatedness, $q<v\vee v<q^{\prime}$. In the left case $q<v$ we are done. In the right case, again by roundedness, there exists $r:\mathbf{Q}$ with $v<r<q^{\prime}$. By $(q^{\prime}-r)$-closeness of $u$ and $v$, there exist $s,s^{\prime}:\mathbf{Q}$ with $s^{\prime}<v<s+(q^{\prime}-r)$ and $s<u<s^{\prime}+(q^{\prime}-r)$. Hence $s^{\prime}<v<r$ and $q^{\prime}<u<s^{\prime}+(q^{\prime}-r)$, hence $q^{\prime}-r<q^{\prime}-r$, a contradiction.

The first distance law follows from the definition of $\operatorname{\mathsf{rat}}$ and the fact that $\operatorname{\mathsf{rat}}(q-r)=\operatorname{\mathsf{rat}}(q)-\operatorname{\mathsf{rat}}(r)$. The remaining three distance laws can be shown by applying Lemma 22. ∎

2.6 Euclidean reals

Let $R$ be a subtype of ${\mathbf{R}_{\mathbf{D}}}$. Viewing $R$ as a type with an embedding into ${\mathbf{R}_{\mathbf{D}}}$, we assign the premetric of ${\mathbf{R}_{\mathbf{D}}}$ to $R$ by restriction.

Lemma 23**.**

Limits in ${\mathbf{R}_{\mathbf{D}}}$, seen as a premetric space, are unique, in the sense that the type of elements which are limits of a given Cauchy approximation is a proposition. Hence the $\operatorname{\mathsf{lim}}$ function of the Cauchy structure of ${\mathbf{R}_{\mathbf{D}}}$ can be restricted to $R$.

Proof.

Let $x:\mathcal{C}_{\mathbf{R}_{\mathbf{D}}}$, and let $u$ and $v$ be limits of $x$. Using the definition of the premetric on ${\mathbf{R}_{\mathbf{D}}}$, and in particular because it satisfies a triangle inequality, we see that $\forall(\varepsilon,\theta:\mathbf{Q}_{+}).u\sim_{2\varepsilon+2\theta}v$, and hence $\forall(\varepsilon:\mathbf{Q}_{+}).u\sim_{\varepsilon}v$, so $u=v$ by an application of $\operatorname{\mathsf{eq}}$. ∎

Definition 24** (Escardo and Simpson [2]).**

The type ${\mathbf{R}_{\mathbf{E}}}$ of Euclidean reals is the smallest Cauchy complete subset of the Dedekind reals containing the rational numbers.

Of course, this type can be constructed as the meet (as in Lemma 6) of the subtypes of the Dedekind reals which are Cauchy complete and contain the rationals.

Lemma 25**.**

${\mathbf{R}_{\mathbf{E}}}$* is Cauchy complete.*

Proof.

The $\operatorname{\mathsf{lim}}$ map is inherited from the Cauchy structure on ${\mathbf{R}_{\mathbf{D}}}$ as in Lemma 23, and the proof of Theorem 20 that this map computes limits also applies to ${\mathbf{R}_{\mathbf{E}}}$. ∎

Proposition 26**.**

The Cauchy structure on ${\mathbf{R}_{\mathbf{D}}}$ restricts to a Cauchy structure on ${\mathbf{R}_{\mathbf{E}}}$.

Proof.

The $\operatorname{\mathsf{rat}}$ map restricts straightforwardly, $\operatorname{\mathsf{lim}}$ is Lemma 23, $\operatorname{\mathsf{eq}}$ follows from (2) in Definition 2, and the distance laws by the fact that the premetric on ${\mathbf{R}_{\mathbf{E}}}$ is just the restriction of the premetric on ${\mathbf{R}_{\mathbf{D}}}$. ∎

Corollary 27**.**

The inclusion of ${\mathbf{R}_{\mathbf{E}}}$ in ${\mathbf{R}_{\mathbf{D}}}$ can be given the structure of a Cauchy structure map.

Proof.

Straightforward. ∎

3 Equivalence of the HoTT reals and the Euclidean reals

Escardó and Simpson [2] showed that the Euclidean real interval is an interval object in any elementary topos. They carried out the proof in the type theory for toposes as described in e.g. [4], known as the internal language or higher-order predicate logic. As discussed in [7] (see also [3, Section 3.2]), constructions and proofs in such a language can be translated to univalent type theory with propositional resizing. In this way, we get that in the category of sets of any universe, the Euclidean real interval is an interval object. To complete our argument, we show that the types of HoTT reals and Euclidean reals are equivalent.

Proposition 28**.**

${\mathbf{R}_{\mathbf{C}}}\simeq{\mathbf{R}_{\mathbf{E}}}$.

Proof.

We will apply Lemma 5 to the following, where we have yet to establish the maps and commutativity conditions.

{{\mathbf{R}_{\mathbf{C}}}}$${{\mathbf{R}_{\mathbf{E}}}}$${\bigcirc}$${{\mathbf{R}_{\mathbf{D}}}}$$\scriptstyle{g}$$\scriptstyle{i_{C}}$$\scriptstyle{f}$$\scriptstyle{i_{E}}

As all three corners of the triangle have an assigned Cauchy structure, we will establish some of those maps and the commutativity conditions by considering the Cauchy structures.

The embedding $i_{E}:{\mathbf{R}_{\mathbf{E}}}\hookrightarrow{\mathbf{R}_{\mathbf{D}}}$ is given by the definition of ${\mathbf{R}_{\mathbf{E}}}$ as an intersection of subsets of ${\mathbf{R}_{\mathbf{D}}}$. This is a Cauchy structure map as per Corollary 27.

Theorem 11.3.50 in the HoTT book constructs the embedding $i_{C}:{\mathbf{R}_{\mathbf{C}}}\to{\mathbf{R}_{\mathbf{D}}}$ as a Cauchy structure morphism. Hence, by the equivalence described in Section 2, we can equivalently see ${\mathbf{R}_{\mathbf{C}}}$ as a Cauchy complete subtype (as in 2.6) of the Dedekind reals containing the rationals. Thus we additionally obtain $f:{\mathbf{R}_{\mathbf{E}}}\to{\mathbf{R}_{\mathbf{C}}}$. The commutativity condition $i_{C}\circ f=i_{E}$ simply expresses that our inclusions are canonical, which they are.

By homotopy-initiality of the HoTT reals, we obtain $g:{\mathbf{R}_{\mathbf{C}}}\to{\mathbf{R}_{\mathbf{E}}}$, and by the fact that Cauchy structure morphisms are closed under composition, using homotopy-initiality once more, we obtain the commutativity condition $i_{E}\circ g=i_{C}$.

Hence we have constructed the maps $f$, $g$, $i_{C}$ and $i_{E}$, as well as the commutativity conditions, so by Lemma 5 we are done. ∎

Corollary 29**.**

The interval in the HoTT reals is an interval object.

4 Conclusion

We proved that the interval in the HoTT reals satisfies the universal property of an interval object. We showed this by first proving that the type of HoTT reals is equivalent to the type of Euclidean reals, which is the least Cauchy complete subset of the Dedekind reals containing the rationals. Then, since we are working in a univalent type theory with propositional resizing, we were able to interpret the theorem of Escardó and Simpson that the interval in the Euclidean reals is an interval object, which makes the interval in the HoTT reals into an interval object.

Limits of Cauchy approximations are interdefinable with iterated midpoints of arbitrary sequences[1, Section 4]. This suggests that it may be possible to show that the interval in the HoTT reals is an interval object directly.