[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Sequential convergence and premetrics} A predicate $P$ on $A$ is a subsingleton-valued type family $P$ indexed by elements of $A$. A binary relation $R$ on $A$ and $B$ is a subsingleton-valued type family $R$ jointly indexed by elements of $A$ and elements of $B$. A binary relation $R$ is functional if for every element $a:A$ the type of all elements $b:B$ such that there is a witness $p:R(a, b)$ is a subsingleton. A **sequential convergence space** is a type $S$ with a binary relation $\mathrm{isLimit}(x, b)$ indexed by sequence $x:\mathbb{N} \to S$ and element $b:S$. Given an sequence $x:\mathbb{N} \to S$, an element $b:S$ is a **limit** of $x$ if there is a witness $p:\mathrm{isLimit}(x, b)$. A sequential convergence space is **sequentially Hausdorff** if the binary relation is a functional relation. Now, let $T$ be a type. A **$T$-premetric space** is a type $S$ with a ternary relation $a \sim_\epsilon b$ indexed by elements $a:S$, $b:S$, and $\epsilon:T$. Every $T$-premetric space is a sequential convergence space with $$\mathrm{isLimit}(x, b) \coloneqq \forall \epsilon:T.\exists N:\mathbb{N}.\forall n:\mathbb{N}.(n \geq N) \to (x(n) \sim_\epsilon b)$$ Given a $T$-premetric space $(S, \sim)$ and a sequence $x:\mathbb{N} \to S$, a **modulus of Cauchy convergence** is a function $M:T \to \mathbb{N}$ with a witness $$p(M, x):\forall \epsilon:T.\forall m:\mathbb{N}.\forall n:\mathbb{N}.((m \geq M(\epsilon)) \wedge (n \geq M(\epsilon))) \to (x(m) \sim_\epsilon x(n))$$ A function $f:T \to S$ is a **Cauchy approximation** if it comes with a sequence $x:\mathbb{N} \to S$ and a modulus of Cauchy convergence $M:T \to \mathbb{N}$ and an identity $p:x \circ M =_{T \to S} f$. A $T$-premetric space $S$ is **sequentially Cauchy complete** if every sequence with a modulus of Cauchy convergence has a unique limit. \section{sequentially complete ordered integral domains} An ordered integral domain is a commutative ring $R$ with a strict linear order $\lt$ such that the monoid of regular elements $\mathrm{Rel}(R)$ is the set of all elements greater than or less than zero: $$\mathrm{Rel}(R) \simeq \sum_{a:R} (a \lt 0) \vee (0 \lt a)$$ category: redirected to nlab