[[!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 Cauchy complete ordered integral domains} Given a commutative ring $R$, an element $a:R$ is regular if for all $b:R$, and $c:R$ the canonical functions $$\mathrm{idtoleftmul}(a, b, c):(b =_R c) \to (a \cdot b =_R a \cdot c)$$ $$\mathrm{idtorightmul}(a, b, c):(b =_R c) \to (b \cdot a =_R c \cdot a)$$ are equivalences: $$\mathrm{isRegular}(a) \coloneqq \prod_{b:A} \prod_{c:A} \mathrm{isEquiv}(\mathrm{idtoleftmul}(a, b, c)) \times \mathrm{isEquiv}(\mathrm{idtorightmul}(a, b, c))$$ We denote the type of regular elements in $R$ as $\mathrm{Rel}(R)$ $$\mathrm{Rel}(R) \coloneqq \sum_{a:A} \mathrm{isRegular}(a)$$ An ordered integral domain is a commutative ring $R$ with a predicate $\mathrm{isPositive}$ such that * zero is not positive * the negation of a positive element is not positive * given elements $a:R$ and $b:R$; if $a$ is positive, then either $b$ is positive or $a - b$ is positive * if both an element $a$ and its negation $-a$ are not positive, then $a$ is equal to zero. * one is positive * the product of two positive elements is positive * the sum of two positive elements is positive * every element $a:R$ is regular if and only if it is positive or its negation is positive: $$\mathrm{isRegular}(a) \simeq \mathrm{isPositive}(a) \vee \mathrm{isPositive}(-a)$$ We define the type of positive elements of $R$ as $$R_+ \coloneqq \sum_{a:R} \mathrm{isPositive}(a)$$ and the premetric $a \sim_\epsilon b$ indexed by $a:R$, $b:R$, and $\epsilon:R_+$ as $$a \sim_\epsilon b \coloneqq \mathrm{isPositive}(\epsilon - (a - b)) \wedge \mathrm{isPositive}(-(\epsilon - (a - b)))$$ category: redirected to nlab