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

Showing changes from revision #6 to #7: Added | ~~Removed~~ | ~~Chan~~ged

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 term $l:S$ is a limit of a net $x: I \to S$ is or a that ~~term~~ $l x : S$ ~~l:S~~ x ~~with~~converges to $l$ if $l$ comes with a term

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

Cauchy approximations

Let $A$ be a dense Archimedean ordered abelian group with a point $1:A$ and a term $\zeta: 0 \lt 1$ . Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the positive cone? of $A$ .

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

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

In convergence spaces

…

Sequences

A limit of a sequence is a limit of a net that happens to be a sequence.