[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] By real number we mean modulated multivalued Cauchy real number. \section{Definition of the real numbers} \begin{definition} A premetric on a type $R$ is a ternary relation $(-) \sim_{(-)} (-):R \times \mathbb{Q} \times R \to \Omega$. \end{definition} \section{References} * {#Booij20} [[Auke Booij]], *Analysis in Univalent Type Theory* (2020) [[etheses:10411](http://etheses.bham.ac.uk/id/eprint/10411), [pdf](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf)] category: redirected to nlab