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

Definition
See also

Definition

In premetric spaces

Let $T$ be a directed type, and let $S$ be a $T$ -premetric space. Given a directed type $I$ , a net $x: I \to S$ is a Cauchy net if

x:I \to S \vdash c(x):\prod_{\epsilon:T} \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 $T$ be a directed type and codirected type where the directed type operation $\oplus$ is associative, and let $S$ be a $T$ -premetric space. A net $x: T \to S$ is a $T$ -Cauchy approximation if

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

Every $T$ -Cauchy approximation is a Cauchy net indexed by $T$ . This is because $T$ is a codirected type, with $N:T$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:T$ and $\eta:T$ . $\epsilon:R_{+}$ is defined as $\epsilon \coloneqq \delta \oplus \eta$ .

In Cauchy spaces

…

Cauchy sequences

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