## Definition ## Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. The __HoTT book real numbers__ $\mathbb{R}_H$ are a homotopy initial $R_{+}$-[[Cauchy structure]], i.e. an $R_{+}$-Cauchy structure such that for every other $R_{+}$-Cauchy structure $S$, the type of $R_{+}$-Cauchy structure homomorphisms with domain $\mathbb{R}_H$ and codomain $S$ is [[contractible]]. ### As a higher inductive-inductive type ### Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. The __HoTT book real numbers__ $\mathbb{R}_H$ are inductively generated by the following: * a function $inj: R \to \mathbb{R}_H$ * a function $lim: C(\mathbb{R}_H, R_{+}) \to \mathbb{R}_H$, where $C(\mathbb{R}_H, R_{+})$ is the type of $R_{+}$-indexed [[net]]s in $\mathbb{R}_H$ that are $R_{+}$-[[Cauchy approximation]]s. * a dependent family of terms $$a:\mathbb{R}_H, b:\mathbb{R}_H \vdash eq_{\mathbb{R}_H}(a, b): \Vert \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_{\mathbb{R}_H} b)$$ and the $R_{+}$-[[premetric]] type family $\sim$ is simultaneously inductively generated by the following: * a dependent family of terms $$a:R, b:R, \epsilon:R_{+} \vdash \mu_{R, R}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$$ * a dependent family of terms $$a:R, b:C(\mathbb{R}_H, R_{+}), \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{R, C(\mathbb{R}_H, R_{+})}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))$$ * a dependent family of terms $$a:C(\mathbb{R}_H, R_{+}), b:R, \delta:R_{+}, \epsilon:R_{+} \vdash \mu_{C(\mathbb{R}_H, R_{+}), R}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))$$ * a dependent family of terms $$a:C(\mathbb{R}_H, R_{+}), b:C(\mathbb{R}_H, R_{+}), \delta:R_{+}, \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{C(\mathbb{R}_H, R_{+}), C(\mathbb{R}_H, R_{+})}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$$ * a dependent family of terms $$a:R, b:R, \epsilon:R_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)$$ ## See also ## * [[Cauchy real numbers]] * [[premetric space]] ## References ## * Auke B. Booij, Analysis in univalent type theory ([pdf](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf)) * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)