# Homotopy Type Theory limit of a function > history (Rev #13, changes)

Showing changes from revision #12 to #13: Added | Removed | Changed

# Contents

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:

$\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isLimit(c, x) \times isLimit(L, f \circ x)$

where

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

$\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit_S(x, c) \times isLimit_T(f \circ x, L)$

### In function limit spaces

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

$hasLimitApproaching(f, c) \coloneqq \Vert \sum_{L:T} \lim_{x \to c} f(x) = L\Vert$

We define the type of functions with limits approaching $c$ as the dependent type

$FuncWithLim(S, T)(c) \coloneqq \sum_{f:S \to T} hasLimitApproaching(f, c)$