[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] finite mathematics. One does not have the natural numbers for mathematics. Instead, one has the potentially infinite sequence of types: $$(\mathbb{0} \to \mathbb{2}) \to (\mathbb{1} \to \mathbb{2}) \to (\mathbb{2} \to \mathbb{2}) \to ((\mathbb{2} + \mathbb{1}) \to \mathbb{2}) \ldots$$ for arithmetic operations in binary, and $$(\mathbb{0} \to \mathbb{10}) \to (\mathbb{1} \to \mathbb{10}) \to (\mathbb{2} \to \mathbb{10}) \to ((\mathbb{2} + \mathbb{1}) \to \mathbb{10}) \ldots$$ for decimal. Type theory (dependent function types, dependent sum types, identity types, function extensionality) -> Predicate logic -> Set theory -> Number theory category: redirected to nlab