[[!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. category: redirected to nlab