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

Showing changes from revision #4 to #5: 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 limit of a net $x: I \to S$ is a term $l:S$ with

\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 ~~abelian~~ dense ~~group~~ ~~with~~ a ~~point~~ ~~$1:A$~~ Archimedean ordered abelian group , with a point~~strict order~~ $1:A$ and a term $ζ : 0 < 1$ \zeta: 0 \lt 1 , . a Let ~~term~~ $ζ A_{+} : ≔ \sum_{a : A} (0 < 1 a)$ ~~\zeta:~~ A_{+} 0 \coloneqq \sum_{a:A} (0 \lt 1 a) ~~and~~ be a the ~~family~~ of ~~dependent~~ ~~terms~~positive cone? of $A$ .

~~$a:A, b:A \vdash \alpha(a, b):(0 \lt a) \times (0 \lt b) \to (0 \lt a + b)$~~

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

~~Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the positive cone? of $A$ .~~

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

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