[[!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. The problem is in defining zero-divisor in a ring. However, we can define the nilradical of the ring to be trivial, that is, $$x:R, n:\mathbb{N}, p:x^{n + 1} =_R 0 \vdash q(x, n, p):x =_R 0$$ and we could do the same with finite products: $$x:R, y:R, m:\mathbb{N}, n:\mathbb{N}, p:x^{m + 1} \cdot y^{n + 1} =_R 0 \vdash q(x, y, m, n, p):(x =_R 0) \vee (y =_R 0)$$ category: redirected to nlab