< [[nlab:Sandbox]] I don't care about any of the Dedekind reals anymore, nor about LPO, nor about coherent real numbers. * We assume an arithmetic $\Pi$-pretopos where the Cauchy quotient functor on Archimedean ordered Heyting integral domains is idempotent. Purely constructive real analysis... [[!redirects Sandbox > history]]