< [[nlab:Sandbox]] We define the Cauchy real numbers to be the Cauchy completion of the rational numbers, which are defined impredicatively using Cauchy nets and polymorphism. This is a higher inductive-inductive type. A *premetric space* is a type $A$ equipped with a ternary relation $x:A, y:A, \epsilon:\mathbb{Q}_+ \vdash \mathrm{tol}(x, y, \epsilon)$ with the interpretation that $x$ and $y$ are $\epsilon$-tolerant. A *directed type* is an inhabited type $B$ with a preorder $\mathrm{leq}:C \hookrightarrow (B \times B)$ such that for all $x:B$ and $y:B$, there exists $z:B$, $c:C$, and $d:C$ such that $\mathrm{leq}(c) = (x, z)$ and $\mathrm{leq}(d) = (y, z)$. A *net* in a type $A$ is a function $v:B \to A$ from a directed type $B$ to $A$. A *modulus of convergence* for a net $v:B \to A$ is a function $\alpha:\mathbb{Q}_+ \to B$ such that for all positive rational numbers $\epsilon:\mathbb{Q}_+$ and elements $i:B$, $j:B$, $\alpha(\epsilon) \leq i$ and $\alpha(\epsilon) \leq j$ imply that $R(v(i), v(j), \epsilon)$. A *Cauchy net* is a net $v:B \to A$ with a modulus of convergence $\alpha:\mathbb{Q}_+ \to B$. A *limit* of a Cauchy net is an element $c:A$ such that for all positive rational numbers $\epsilon:\mathbb{Q}_+$ and elements $i:B$, $\alpha(\epsilon) \leq i$ implies that $R(v(i), c, \epsilon)$. A premetric space is *complete* if every net with a modulus of convergence has a limit. [[!redirects Sandbox &gt; history]]