Homotopy Type Theory limit of a function > history (Rev #8)

Definition
See also

Definition

In rational numbers

Let $\mathbb{Q}$ be the rational numbers and let $\mathbb{Q}_{+}$ be the positive rational numbers. The limit of a function $f:\mathbb{Q} \to \mathbb{Q}$ approaching a term $c:\mathbb{Q}$ is a term $L:\mathbb{Q}$ such that for all directed types $I$ and nets $x:I \to \mathbb{Q}$ 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 \mathbb{Q}} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - c \vert \lt \epsilon) \Vert

isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon) \Vert

The limit is usually written as

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

In Archimedean ordered fields

Let $F$ be an Archimedean ordered field and let $F_{+}$ be the positive terms of $F$ . 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:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - c \vert \lt \epsilon) \Vert

isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon) \Vert

The limit is usually written as

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

Most general definition

Let $S$ be a type with a predicate $isLimit_S$ between the type of all nets in $S$

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

and $S$ itself, and let $T$ be a type with a predicate $isLimit_T$ between the type of all nets in $T$

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

and $T$ itself.

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)

Homotopy Type Theory limit of a function > history (Rev #8)

Contents

Definition

In rational numbers

In Archimedean ordered fields

Most general definition

See also