## Definition ### Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. The __generalized Cauchy real numbers__ $\mathbb{R}_\mathcal{U}$ are inductively generated by the following: * a function $inj: \left(\sum_{I:\mathcal{U}} C(I, R)\right) \to \mathbb{R}_\mathcal{U}$, where $$C(I, R) \coloneqq isDirected(I) \times \sum_{x:I \to R} isCauchy(x)$$ is the type of all [[Cauchy net]]s with [[directed type|index type]] $I$ and values in $R$. * a dependent family of terms $$a:C(I, R), b:C(J, R) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (inj(a) =_{\mathbb{R}_\mathcal{U}} inj(b))$$ where $I$ and $J$ are directed types and the equivalence relation on Cauchy nets $isEq_{\mathbb{R}_\mathcal{U}}(a, b)$ is defined as $$isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:R_{+}} \Vert \sum_{M:I} \prod_{i:I} \Vert \sum_{N:J} \prod_{j:J} (i \geq M) \times (j \geq N) \times (\vert a_i - b_j \vert \lt \epsilon) \Vert \Vert$$ * a term $\tau: isSet(\mathbb{R}_\mathcal{U})$ ## See also ## * [[Cauchy real numbers (disambiguation)]] * [[HoTT book real numbers]] * [[Cauchy real numbers]] * [[premetric space]]