[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents types with decidable equality $$a:A, b:A \vdash p(a, b):(a =_A b) + \neg (a =_A b)$$ \section{Commutative rings} A commutative ring is a set $R$ with * a dependent term $x:R, y:R \vdash x + y:R$ * a term $0:R$ * a dependent term $x:R \vdash -x:R$ * a dependent term $x:R, y:R \vdash x \cdot y:R$ * a term $1:R$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_+(x, y, z):x + (y + z) =_R (x + y) + z$ * a dependent term $x:R \vdash \mathrm{lunit}_+(x):0 + x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_+(x):x + 0 =_R x$ * a dependent term $x:R \vdash \mathrm{linv}_+(x):(-x) + x =_R 0$ * a dependent term $x:R \vdash \mathrm{rinv}_+(x):x + (-x) =_R 0$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_+(x, y):x + y =_R y + x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{assoc}_\cdot(x, y, z):x \cdot (y \cdot z) =_R (x \cdot y) \cdot z$ * a dependent term $x:R \vdash \mathrm{lunit}_\cdot(x):1 \cdot x =_R x$ * a dependent term $x:R \vdash \mathrm{runit}_\cdot(x):x \cdot 1 =_R x$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{ldist}_\cdot(x, y, z):x \cdot (y + z) =_R x \cdot y + x \cdot z$ * a dependent term $x:R, y:R, z:R \vdash \mathrm{rdist}_\cdot(x, y, z):(y + z) \cdot x =_R y \cdot x + z \cdot x$ * a dependent term $x:R, y:R \vdash \mathrm{comm}_\cdot(x, y):x \cdot y =_R y \cdot x$ \section{Apart commutative rings} An apart commutative ring is a commutative ring $R$ with a predicate $\mathrm{isApartFromZero}(a)$ indicating that element $a:R$ is positive, such that * zero is not apart from zero * given element $a:R$, if $a$ is apart from zero, then $-a$ is apart from zero * given elements $a:R$ and $b:R$; if $a$ is apart from zero, then either $b$ is apart from zero or $a - b$ is apart from zero * one is apart from zero * the product of two elements apart from zero is apart from zero Every apart commutative ring has an apartness relation given by $a \# b \coloneqq \mathrm{isApartFromZero}(b - a)$ and an equivalence relation given by $a \approx b \coloneqq \neg (a \# b)$. \section{Apart 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))$$ An apart integral domain is an apart commutative ring $R$ such that for all elements $a:R$, $a$ is regular if and only if it is apart from zero: $$\mathrm{isRegular}(a) \simeq \mathrm{isApartFromZero}(a)$$ \section{Apart field} Given a commutative ring $R$, an element $a:R$ is invertible if the type of all $b:B$ such that $a \cdot b =_R 1$ is contractible $$\mathrm{isInvertible}(a):\mathrm{isContr}\left(\sum_{b:B} a \cdot b =_R 1\right)$$ An apart field is an apart commutative ring $R$ such that for all elements $a:R$, $a$ is invertible if and only if it is apart from zero: $$\mathrm{isInvertible}(a) \simeq \mathrm{isApartFromZero}(a)$$ \section{Ordered commutative rings} An ordered commutative ring is a commutative ring $R$ with a predicate $\mathrm{isPositive}(a)$ indicating that element $a:R$ is positive, such that * zero is not positive * given element $a:R$, if $a$ is positive, then $-a$ is not positive * given elements $a:R$ and $b:R$; if $a$ is positive, then either $b$ is positive or $a - b$ is positive * one is positive * the sum of two positive elements is positive * the product of two positive elements is positive Every ordered commutative ring has a strict order given by $a \lt b \coloneqq \mathrm{isPositive}(b - a)$ and a preorder given by $a \leq b \coloneqq \neg (b \lt a)$. \section{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))$$ An ordered integral domain is an ordered commutative ring $R$ such that for all elements $a:R$, $a$ 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)$$ \section{Ordered field} Given a commutative ring $R$, an element $a:R$ is invertible if the type of all $b:B$ such that $a \cdot b =_R 1$ is contractible $$\mathrm{isInvertible}(a):\mathrm{isContr}\left(\sum_{b:B} a \cdot b =_R 1\right)$$ An ordered field is an ordered commutative ring $R$ such that for all elements $a:R$, $a$ is invertible if and only if it is positive or its negation is positive: $$\mathrm{isInvertible}(a) \simeq \mathrm{isPositive}(a) \vee \mathrm{isPositive}(-a)$$ category: redirected to nlab