[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] coherent mathematics is still the future We can inductively define both equality $x =_\mathbb{N} y$ and apartness $x \#_\mathbb{N} y$ on the natural numbers by double induction on the natural numbers, and then prove that $\mathrm{deceq}(x, y):(x =_\mathbb{N} y) + (x \#_\mathbb{N} y)$. Indeed, we can require every set $A$ have both equality $x =_A y$ and apartness $x \#_A y$ and require that every pair of elements is either equal to or apart from each other $\mathrm{deceq}(x, y):(x =_A y) + (x \#_A y)$. This makes it into a Boolean pretopos, which is good enough for classical predicative mathematics. ## Mathematical structures Basic structures * A set is a type where every identity type is a proposition. * An apartness type is a type equipped with an apartness relation, a propositional binary type family which is irreflexive, asymmetric, and comparative. If the type is a set it is called an apartness set. * A decidable apartness set is an apartness set where given two elements the sum of the identity type and the apartness relation always contains an element. * A set has a choice operator if from every witness of its propositional truncation one could construct an element of the set. This implies that it is a decidable apartness space. Move on from ideals, we should study anti-ideals. Move on from set rings, we should study apartness rings. Most relevant rings have apartness structure on them, such as the integers, the rational numbers, and the real numbers. The reason why for the study of anti-ideals is because of the existence of local rings and ordered local rings means that one has apartness independent of equality. An apartness set $S$ is discrete if $a \in S, b \in S \vdash (a = b) \vee (a \# b)$ An anti-ideal in an apartness ring $R$ is an $\#$-open subset $A \subseteq R$ such that * $a \# 0$ * $a + b \in A$ implies that $a \in A$ or $b \in A$ * $a \cdot b \in A$ implies that $a \in A$ and $b \in A$ A ring is local if the set of invertible elements forms an anti-ideal. A ring is a field if it is a discrete local ring. category: redirected to nlab