#Contents# * table of contents {:toc} ## Definition ## ### In rational numbers ### Let $\mathbb{Q}$ be the [[rational numbers]] and let $\mathbb{Q}_{+}$ be the type of positive rational numbers. Given a [[directed type]] $I$, a term $l:\mathbb{Q}$ is a __limit of a net__ $x: I \to \mathbb{Q}$ or that $x$ __converges to__ $l$ if $l$ comes with a term $$\lambda: \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert$$ The type of all limits of a net is defined as $$\lim x \coloneqq \sum_{l:\mathbb{Q}} \left(\prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert\right)$$ A __limit of a sequence__ $a:\mathbb{N} \to \mathbb{Q}$ is usually written as $$\lim_{x \to \infty} a(x)$$ ### In Archimedean ordered fields ### Let $F$ be an [[Archimedean ordered field]] and let $F_{+}$ be the type of positive rational numbers. Given a [[directed type]] $I$, a term $l:F$ is a __limit of a net__ $x: I \to F$ or that $x$ __converges to__ $l$ if $l$ comes with a term $$\lambda: \prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert$$ The type of all limits of a net is defined as $$\lim x \coloneqq \sum_{l:F} \left(\prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - l \vert \lt \epsilon) \Vert\right)$$ A __limit of a sequence__ $a:\mathbb{N} \to F$ is usually written as $$\lim_{x \to \infty} a(x)$$ ### Most general definition ### Let $S$ be a type with a [[predicate]] $\to$ between the type of all nets in $S$ $$\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)$$ and $S$ itself. Given a [[directed type]] $I$, a term $l:S$ is a __limit of a net__ $x: I \to S$ or that $x$ __converges to__ $l$ if the proposition $x \to l$ is [[contractible]]. The type of all limits of a net is defined as $$\lim x \coloneqq \sum_{l:S} x \to l$$ ## See also ## * [[net]] * [[premetric space]] * [[Hausdorff space]] * [[limit of a function]] * [[modulus of Cauchy convergence]] * [[Cauchy structure]] * [[Cauchy approximation]] * [[HoTT book real numbers]]