# Homotopy Type Theory generalized Cauchy real numbers > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

# Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

## Definition

### In set theory

Let $\mathbb{Q}$ be the rational numbers and let

$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$

be the set of positive rational numbers. Let $I$ be a directed set and

$C(I, \mathbb{Q}) \coloneqq \{x \in \mathbb{Q}^I \vert \forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (x_i \sim_{\epsilon} x_j)\}$

is the set of all Cauchy nets with index set $I$ and values in $\mathbb{Q}$. Let

$CauchyNetsIn(\mathbb{Q}) \coloneqq \bigcup_{I \in Ob(DirectedSet_\mathcal{U})} C(I, \mathbb{Q})$

be the (large) set of all Cauchy nets in $\mathbb{Q}$ in a universe $\mathcal{U}$, where $DirectedSet_\mathcal{U}$ is the category of all directed sets in $\mathcal{U}$.

Let the relation $\equiv_{I, J}$ in the Cartesian product $C(I, \mathbb{Q}) \times C(J, \mathbb{Q})$ for directed sets $I$ and $J$ be defined as

$a \equiv_{I, J} b \coloneqq \forall \epsilon \in \mathbb{Q}_{+}, \exists M \in I. \forall i \in I. \exists N \in J. \forall j \in J. (i \geq M) \wedge (j \geq N) \wedge (\vert a_i - b_j \vert \lt \epsilon)$

Let a generalized Cauchy algebra be defined as a set $A$ with a function $\iota \in {A}^{CauchyNetsIn(\mathbb{Q})}$ such that

$\forall I \in Ob(DirectedSet_\mathcal{U}). \forall J \in Ob(DirectedSet_\mathcal{U}). \forall a \in C(I, \mathbb{Q}). \forall b \in C(J, \mathbb{Q}). (a \equiv_{I, J} b) \implies (\iota(a) = \iota(b))$

A generalized Cauchy algebra homomorphism is a function $f:B^A$ between Cauchy algebras $A$ and $B$ such that

$\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)$

The category of generalized Cauchy algebras is the category $GCAlg$ whose objects $Ob(GCAlg)$ are generalized Cauchy algebras and whose morphisms $Mor(GCAlg)$ are generalized Cauchy algebra homomorphisms. The set of generalized Cauchy real numbers, denoted $\mathbb{R}$, is defined as the initial object in the category of Cauchy algebras.

### In homotopy type theory

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 generalized Cauchy real numbers $\mathbb{R}_\mathcal{U}$ are inductively generated by the following:

• a function $\iota: \left(\sum_{I:\mathcal{U}} C(I, \mathbb{Q})\right) \to \mathbb{R}_\mathcal{U}$, where

$C(I, \mathbb{Q}) \coloneqq isDirected(I) \times \sum_{x:I \to \mathbb{Q}} isCauchy(x)$

is the type of all Cauchy nets with index type $I$ and values in $\mathbb{Q}$.

• a dependent family of terms

$a:C(I, \mathbb{Q}), b:C(J, \mathbb{Q}) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (\iota(a) =_{\mathbb{R}_\mathcal{U}} \iota(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:\mathbb{Q}_{+}} \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})$