#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### Let $F$ be an [[Archimedean ordered field]] and let $$F_{+} \coloneqq \sum_{a:F} 0 \lt a$$ be the positive elements in $F$. $F$ is *sequentially Cauchy complete* if every Cauchy sequence in $F$ converges: $$isCauchy(x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)$$ $$isLimit(x, l) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$$ $$\forall x \in F^\mathbb{N}. isCauchy(x) \wedge \exists l \in F. isLimit(x, l)$$ The set of __HoTT book real numbers__ $\mathbb{R}_H$ is the initial [[sequentially Cauchy complete]] [[Archimedean ordered field]]. The set of __HoTT book real numbers__ $\mathbb{R}_H$ is the initial object in the [[category of Cauchy structures]] and [[Cauchy structure homomorphism]]s. ### In homotopy type theory ### The __HoTT book real numbers__ $\mathbb{R}_H$ are a homotopy initial [[Cauchy structure]], i.e. a Cauchy structure such that for every other Cauchy structure $S$, the type of [[Cauchy structure homomorphism]]s with domain $\mathbb{R}_H$ and codomain $S$ is [[contractible]]. #### As a higher inductive-inductive type #### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$ be the positive rational numbers. The __HoTT book real numbers__ $\mathbb{R}_H$ are inductively generated by the following: * a function $inj: \mathbb{Q} \to \mathbb{R}_H$ * a function $lim: C(\mathbb{R}_H) \to \mathbb{R}_H$, where $C(\mathbb{R}_H)$ is the type of [[Cauchy approximation]]s in $\mathbb{R}_H$. * a dependent family of terms $$a:\mathbb{R}_H, b:\mathbb{R}_H \vdash eq_{\mathbb{R}_H}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \right) \to (a =_{\mathbb{R}_H} b)$$ and the [[premetric]] type family $\sim$ is simultaneously inductively generated by the following: * a dependent family of terms $$a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, \mathbb{Q}}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$$ * a dependent family of terms $$a:\mathbb{Q}, b:C(\mathbb{R}_H), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(\mathbb{R}_H)}(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), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), \mathbb{Q}}(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), b:C(\mathbb{R}_H), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), C(\mathbb{R}_H)}(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:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)$$ ## See also ## * [[Cauchy real numbers]] * [[generalized Cauchy real numbers]] * [[Cauchy real numbers (disambiguation)]] * [[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)