#Contents# * table of contents {:toc} ## 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 group]] with a point $1:A$, a [[strict order]] $\lt$, a term $\zeta: 0 \lt 1$ and a family of dependent terms $$a:A, b:A \vdash \alpha(a, b):(0 \lt a) \times (0 \lt b) \to (0 \lt a + b)$$ Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the [[positive cone]] of $A$. 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. ## See also ## * [[premetric space]] * [[modulus of Cauchy convergence]] * [[Cauchy structure]] * [[Cauchy approximation]] * [[HoTT book real numbers]]