#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## 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): \left( \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \right) \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)$$ ### In set theory ### A __premetric space__ is a set $S$ with a ternary relation $\sim$ on the Cartesian product $\mathbb{Q}_{+} \times S \times S$, where $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ is the set of positive rational numbers. A __Cauchy approximation__ in $S$ is an function $x \in S^{\mathbb{Q}_{+}}$, where $S^{\mathbb{Q}_{+}}$ is the set of functions with domain $\mathbb{Q}_{+}$ and codomain $S$, such that $$\forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)$$ The set of all Cauchy approximations is defined as $$C(S) \coloneqq \{x \in S^{\mathbb{Q}_{+}} \vert \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)\}$$ A __Cauchy structure__ is a premetric space $S$ with a function $rat \in S^{\mathbb{Q}_{+}}$ and a function $lim \in S^{C(S)}$ such that $$\forall a \in S.\forall b \in S.((\forall \epsilon \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b)$$ $$\forall a \in \mathbb{Q}.\forall b \in \mathbb{Q}.\forall \epsilon \in \mathbb{Q}_{+}.(\vert a - b \vert \lt \epsilon \implies rat(a) \sim_\epsilon rat(b))$$ $$\forall a \in \mathbb{Q}.\forall b \in C(S).\forall \epsilon \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.(rat(a) \sim_\epsilon b(\eta) \implies rat(a) \sim_{\epsilon + \eta} lim(b))$$ $$\forall a \in C(S).\forall b \in \mathbb{Q}.\forall \epsilon \in \mathbb{Q}_{+}.\forall \delta \in \mathbb{Q}_{+}.(a(\delta) \sim_\epsilon rat(b) \implies lim(a) \sim_{\delta + \epsilon} rat(b))$$ $$\forall a \in C(S).\forall b \in C(S).\forall \epsilon \in \mathbb{Q}_{+}.\forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.(a(\delta) \sim_\epsilon b(\eta) \implies lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$$ For two Cauchy structures $S$ and $T$, a __Cauchy structure homomorphism__ is a function $f\in T^S$ such that $$\forall a \in S.\forall b \in S.\forall \epsilon \in \mathbb{Q}_{+}.(a \sim_{\epsilon} b) \to (f(a) \sim_{\epsilon} f(b))$$ $$\forall r\in \mathbb{Q}.f(rat(r)) = rat(r)$$ $$\forall r\in C(S).f(lim(r)) = lim(f \circ r)$$ $$\forall a \in S.\forall b \in S.(((\forall \epsilon \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b) \implies ((\forall \epsilon \in \mathbb{Q}_{+}.f(a) \sim_\epsilon f(b)) \implies f(a) = f(b))$$ The set of __HoTT book real numbers__ $\mathbb{R}_H$ is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms. ## 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)