[[!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. ## Power series Move on from nilradicals, we should study Jacobson radicals. Move on from ideals, we should study anti-ideals. 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 anti-ideal in an apartness ring $R$ is an $\#$-open subset $A$ such that for all elements $a \in A$, $a \# 0$, $a + b \in A$ implies that $a \in A$ or $b \in A$, and $b \in A$ whenever $a \cdot b \in A$. category: redirected to nlab