[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Algebraic real analysis. * differentiability - preservation of function by the canonical strictly monotonic ring homomorphism from the Dedekind real numbers into an Archimedean ordered Artinian local Dedekind real algebra, and satisfying the truncated Taylor series condition. * continuity - shapewise continuity: the function graph has contractible shape, contractible localization at the Dedekind real numbers. Needed for integration, I think? Also, inverse function theorem. * definite integration - every closed interval in the Dedekind real numbers is a closed midpoint algebra, see Peter Freyd's algebraic real analysis. Let $\mathbb{I} \subseteq \mathbb{R}$ be the unit interval in the real numbers. Let $C(\mathbb{I})$ be the set of all continuous functions on the unit interval. Then there is a function $$\int_{0}^{1}:C(\mathbb{I}) \to C(\mathbb{I})$$ such that $$\int_{0}^{1} \mathrm{const}_0(x) = 0 \quad \int_{0}^{1} \mathrm{const}_1(x) = 1$$ $$\int_{0}^{1} \frac{1}{2} \left(f(x) + g(x)\right) = \frac{1}{2}\left(\int_{0}^{1} f(x)\right) + \frac{1}{2}\left(\int_{0}^{1} g(x)\right)$$ $$\int_{0}^{1} f(x) = \int_{0}^{1} \frac{1}{2} \left(f\left(\frac{1}{2} x\right) + f\left(\frac{1}{2} (1 - x)\right)\right)$$ category: redirected to nlab