Construction of Dedekind reals using higher inductive-inductive types 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?
 A: 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, 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'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.
A: I don't know if it answers your specific question, but as a general discussion of related things I recommend The HoTT reals coincide with the Escardó-Simpson reals by Auke Booij.
