Homotopy Type Theory limit of a net > history (Rev #12, changes)

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

Definition
See also

Definition

In rational numbers

Let $\mathbb{Q}$ be the rational numbers and let $\mathbb{Q}_{+}$ be the type of positive rational numbers. Given a directed type $I$ , a term $l:\mathbb{Q}$ is a limit of a net $x: I \to \mathbb{Q}$ or that $x$ converges to $l$ if $l$ comes with a term

\lambda: \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert

The type of all limits of a net is defined as

\lim x \coloneqq \sum_{l:\mathbb{Q}} \left(\prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert\right)

A limit of a sequence $a:\mathbb{N} \to \mathbb{Q}$ is usually written as

\lim_{x \to \infty} a(x)

In premetric spaces

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ . Let $S$ be a $R_{+}$ -premetric space. Given a directed type $I$ , a term $l:S$ is a limit of a net $x: I \to S$ or that $x$ converges to $l$ if $l$ comes with a term

\lambda: \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert

The type of all limits of a net is defined as

\lim x \coloneqq \sum_{l:S} \left(\prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert\right)

~~A limit of a sequence $a:\mathbb{N} \to S$ is usually written as~~
~~$\lim_{x \to \infty} a(x)$~~

Cauchy approximations

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ .

A limit of a $R_{+}$ -Cauchy approximation $x: R_{+} \to S$ is a term $l:S$ with

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

In Most convergence general spaces definition

… Let $S$ be a type with a predicate $\to$ between the type of all nets in $S$

\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

and $S$ itself.

Given a directed type $I$ , a term $l:S$ is a limit of a net $x: I \to S$ or that $x$ converges to $l$ if the proposition $x \to l$ is contractible.

The type of all limits of a net is defined as

\lim x \coloneqq \sum_{l:S} x \to l

Homotopy Type Theory limit of a net > history (Rev #12, changes)

Contents

Definition

In rational numbers

In premetric spaces

Cauchy approximations

In Most convergence general spaces definition

See also