[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] We should be looking at practical foundations again. We work in a pretopos with function sets, the set of natural numbers, and a terminal Archimedean ordered field satisfying the analytic LPO. We do not believe in the Heine-Borel theorem, and we cannot construct formal topologies, frames, locales, and topological spaces. Instead, we simply work with locally uniformly continuous functions everywhere. category: redirected to nlab