Homotopy Type Theory Cauchy net > history (Rev #13, changes)

Showing changes from revision #12 to #13: Added | ~~Removed~~ | ~~Chan~~ged

Definition
See also

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

Definition

In premetric set spaces theory

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

In premetric spaces

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

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

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

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

~~$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$~~

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

~~Cauchy approximations~~

\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)

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

Cauchy approximations

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

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

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

be the positive rational numbers.

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

x \forall : δ \in ℚ_{+} \to . S \forall ⊢ η c \in (ℚ_{+} x .) : \prod_{δ : R_{+}} \prod_{η : R_{+}} x_{δ} \sim_{δ + η} x_{η}

~~x:\mathbb{Q}_{+}~~ \forall ~~\to~~ \delta S \in ~~\vdash~~ \mathbb{Q}_{+}. ~~c(x):\prod_{\delta:R_{+}}~~ \forall ~~\prod_{\eta:R_{+}}~~ \eta \in \mathbb{Q}_{+}. 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 : \in ℚ_{+}$ ~~N:\mathbb{Q}_{+}~~ N \in \mathbb{Q}_{+} defined as $N \coloneqq \delta \otimes \eta$ for $δ : \in R ℚ_{+}$ ~~\delta:R\mathbb{Q}_{+}~~ \delta \in \mathbb{Q}_{+} and $η : \in ℚ_{+}$ ~~\eta:\mathbb{Q}_{+}~~ \eta \in \mathbb{Q}_{+}. $ϵ : \in ℚ_{+}$ ~~\epsilon:\mathbb{Q}_{+}~~ \epsilon \in \mathbb{Q}_{+} is defined as $\epsilon \coloneqq \delta + \eta$ .

~~In Cauchy spaces~~

In Cauchy spaces

…

In homotopy type theory

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:\mathbb{Q}_{+}} \prod_{\eta:\mathbb{Q}_{+}} 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:\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}$ .

Homotopy Type Theory Cauchy net > history (Rev #13, changes)

Contents

Definition

In premetric set spaces theory

In premetric spaces

Cauchy approximations

Cauchy approximations

In Cauchy spaces

In Cauchy spaces

In homotopy type theory

In premetric spaces

Cauchy approximations

In Cauchy spaces

Cauchy sequences

See also