[[!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 I think we shall take seriously the (classically valid) notion that power series rings represent infinitesimal spaces. we just study Archimedean ordered local rings. category: redirected to nlab