< [[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$. [[!redirects Sandbox &gt; history]]