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

Definition

In Archimedean ordered fields

Let $F$ be an Archimedean ordered field. The limit of a function$f:\F \to F$ approaching a term $c:F$ is a term $L:F$ such that for all directed types $I$ and nets $x:I \to F$ where $c$ is the limit of $x$, $L$ is the limit of $f \circ x$, or written in type theory:

$isLimit(c,x) \coloneqq \prod_{\epsilon:(0, \infty)} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to \left[\sum_{a:(-\epsilon, \epsilon)} x_i - c = a\right]\right]$

$isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:(0, \infty)} \left[\sum_{N:I} \prod_{i:I} (i \geq N) \to \left[\sum_{a:(-\epsilon, \epsilon)} f(x_i) - L = a\right] \right]$

The limit is usually written as

$L \coloneqq \lim_{x \to c} f(x)$

In preconvergence spaces

Let $S$ and $T$ be preconvergence spaces. The limit of a function$f:S \to T$ approaching a term $c:S$ is a term $L:T$ such that for all directed types $I$ and nets $x:I \to S$ where $c$ is a limit of $x$, $L$ is a limit of $f \circ x$, or written in type theory:

Let $T$ be a function limit space and let $S \subseteq T$ be a subtype of $T$. The limit of a function$f:S \to T$ approaching $c:S$ is a term $L:T$ such that the limit of $f$ approaching $c:S$ is equal to $L$: