In the textbook Homotopy Type Theory: Univalent Foundations of Mathematics, the authors give a predicative constructive construction of the initial Cauchy complete reals $\mathbb{R}\_C$ in terms of a higher inductive-inductive type ${\sim}\_C$ defined at the same time as $\mathbb{R}\_C$. Is there a similar construction of the initial Dedekind complete reals $\mathbb{R}\_D$ as a higher inductive-inductive type?



Construction of Dedekind reals using higher inductive-inductive types
The Dedekind reals are constructed as Dedekind cuts in section 11.2 of the HoTT book. A Dedekind cut is a pair $(L,U)$ of subsets of rational numbers $\mathbb{Q}$ satisfying the conditions listed at the beginning of the section. The Dedekind reals as a type are therefore *not* a higher inductive-inductive type, but are rather a **dependent sum** of the form
$$\Sigma (L \,{:}\, P\mathbb{Q}) \,\Sigma (U \,{:}\, P\mathbb{Q}) \; \mathrm{isCut}(L,U).$$
Nevertheless, there is something to be said about predicativity and higher inductive-inductive types. A question arises what we should do about $P \mathbb{Q}$, which is supposed to be the powerset of rational numbers, but HoTT does not have powersets. If you keep reading the section, you will find a discussion of the possibilities, some of which are more impredicative than others.


One of the options listed is to avoid all impredicativity by setting $P \mathbb{Q} = (\mathbb{Q} \to \mathbb{S})$, where $\mathbb{S}$ is the [Sierpinski space](https://en.wikipedia.org/wiki/Sierpi%C5%84ski_space), constructed as a higher inductive-inductive type, namely the *initial $\omega$-frame*. This is the initial lattice with $0$, $1$, binary meets $\wedge$ and countable joins $\bigvee\_{n : \mathbb{N}}$, satisfying the distributivity law $p \wedge \bigvee\_n q\_n = \bigvee\_n (p \wedge q\_n)$.
Note that we require here a higher inductive-inductive construction because one of the operations is infinitary (the finitary algebras are constructed as ordinary higher inductive types, see section 6.11 of the HoTT book).


The resulting notion of predicative Dedekind reals is maybe not what one really wants, but is still quite useful and has been studied, for example by [Davorin Lešnik](https://www.fmf.uni-lj.si/sl/imenik/137/lesnik-davorin/)'s dissertation (if anyone writes to him, ask him to put his PhD up on the web page as it disappeared recently), and by Paul Taylor and myself in [The Dedekind reals in Abstract Stone Duality](http://www.paultaylor.eu/ASD/dedras/).


