Homotopy Type Theory Cauchy net > history (Rev #12)

Definition
See also

Definition

In premetric spaces

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

\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

be the positive rational numbers. Let $S$ be an premetric space. A net $x: I \to S$ is a Cauchy net if

x:I \to S \vdash c(x):\prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert

Cauchy approximations

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

\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

be the positive rational numbers.

A net $x: \mathbb{Q}_{+} \to S$ is a Cauchy approximation if

x:\mathbb{Q}_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta

Every Cauchy approximation is a Cauchy net indexed by $\mathbb{Q}_{+}$ . This is because $\mathbb{Q}_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N:\mathbb{Q}_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:R\mathbb{Q}_{+}$ and $\eta:\mathbb{Q}_{+}$ . $\epsilon:\mathbb{Q}_{+}$ is defined as $\epsilon \coloneqq \delta + \eta$ .

In Cauchy spaces

…

Cauchy sequences

A Cauchy sequence is a Cauchy net whose index type is the natural numbers $\mathbb{N}$ .