[[!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. Not really finite mathematics, but I would rather higher inductive types like the circle types than types with function constructors like the natural numbers or the integers. Formation rules for the circle type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash S^1 \; \mathrm{type}}$$ Introduction rules for the circle type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash b:S^1} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash l:b =_{S^1} b}$$ Elimination rules for the circle type: $$\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_b:C(b) \quad \Gamma \vdash c_l:c_b =_{x:S^1.C(x)}^{(b, b, l)} c_b}{\Gamma \vdash \mathrm{ind}_{S^1}^{x:S^1.C(x)}(c_b, c_l):\prod_{x:S^1} C(x)}$$ Computation rules for the circle type: $$\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_b:C(b) \quad \Gamma \vdash c_l:c_b =_{x:S^1.C(x)}^{(b, b, l)} c_b}{\Gamma \vdash \beta_{S^1}^{b}(c_b, c_l):\mathrm{ind}_{S^1}^{x:S^1.C(x)}(c_b, c_l)(b) =_{C(b)} c_b}$$ $$\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_b:C(b) \quad \Gamma \vdash c_l:c_b =_{x:S^1.C(x)}^{(b, b, l)} c_b}{\Gamma \vdash \beta_{S^1}^{l}(c_b, c_l):\mathrm{apd}_{x:S^1.C(x)}(\mathrm{ind}_{S^1}^{x:S^1.C(x)}(c_b, c_l), b, b, l) =_{c_b =_{x:S^1.C(x)}^{(b, b, l)} c_b} c_l}$$ and for recursion: Elimination rules for the circle type: $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_b:C \quad \Gamma \vdash c_l:c_b =_{C} c_b}{\Gamma \vdash \mathrm{rec}_{S^1}^{C}(c_b, c_l):S^1 \to C}$$ Computation rules for the circle type: $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_b:C \quad \Gamma \vdash c_l:c_b =_{C} c_b}{\Gamma \vdash \beta_{S^1}^{b}(c_b, c_l):\mathrm{rec}_{S^1}^{C}(c_b, c_l)(b) =_{C} c_b}$$ $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_b:C \quad \Gamma \vdash c_l:c_b =_{C} c_b}{\Gamma \vdash \beta_{S^1}^{l}(c_b, c_l):\mathrm{ap}_{C}(\mathrm{rec}_{S^1}^{C}(c_b, c_l), b, b, l) =_{c_b =_{C} c_b} c_l}$$ Double recursion: (b, b), Elimination rules for the circle type: $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{b, b}:C \quad \Gamma \vdash c_{b, l}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, b}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, l}:c_{b, b} =_{C} c_{b, b}}{\Gamma \vdash \mathrm{rec}_{S^1}^{C}(c_{b, b}, c_{b, l}, c_{l, b}, c_{l, l}):(S^1 \times S^1) \to C}$$ Computation rules for the circle type: $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{b, b}:C \quad \Gamma \vdash c_{b, l}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, b}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, l}:c_{b, b} =_{C} c_{b, b}}{\Gamma \vdash \beta_{S^1}^{b, b}(c_b, c_l):\mathrm{rec}_{S^1}^{C}(c_{b, b}, c_{b, l}, c_{l, b}, c_{l, l}, b, b) =_{C} c_{b, b}}$$ $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{b, b}:C \quad \Gamma \vdash c_{b, l}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, b}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, l}:c_{b, b} =_{C} c_{b, b}}{\Gamma \vdash \beta_{S^1}^{b, l}(c_b, c_l):\mathrm{ap}_{C}(\lambda x:S^1.\mathrm{rec}_{S^1}^{C}(c_{b, b}, c_{b, l}, c_{l, b}, c_{l, l}, b, x), b, b, l) =_{c_{b, b} =_{C} c_{b, b}} c_{b, l}}$$ $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{b, b}:C \quad \Gamma \vdash c_{b, l}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, b}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, l}:c_{b, b} =_{C} c_{b, b}}{\Gamma \vdash \beta_{S^1}^{l, b}(c_b, c_l):\mathrm{ap}_{C}(\lambda x:S^1.\mathrm{rec}_{S^1}^{C}(c_{b, b}, c_{b, l}, c_{l, b}, c_{l, l}, x, b), b, b, l) =_{c_{b, b} =_{C} c_{b, b}} c_{l, b}}$$ $$\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_{b, b}:C \quad \Gamma \vdash c_{b, l}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, b}:c_{b, b} =_{C} c_{b, b} \quad \Gamma \vdash c_{l, l}:c_{b, b} =_{C} c_{b, b}}{\Gamma \vdash \beta_{S^1}^{l, l}(c_b, c_l):\mathrm{apbin}_{C}(\mathrm{rec}_{S^1}^{C}(c_{b, b}, c_{b, l}, c_{l, b}, c_{l, l}), b, b, b, b, l, l) =_{c_{b, b} =_{C} c_{b, b}} c_{l, l}}$$ $$\mathrm{rec}_{S^1}^{S^1}(b, l, l, l \bullet l):S^1 \times S^1 \to S^1$$ $$\mathrm{rec}_{S^1}^{S^1}(b, l^{-1}):S^1 \times S^1 \to S^1$$ $$\mathrm{rec}_{S^1}^{S^1}(b, l^{-1}, l, \mathrm{refl}_{S^1}(b)):S^1 \times S^1 \to S^1$$ $$\mathrm{rec}_{S^1}^{S^1}(b, \mathrm{refl}_{S^1}(b), \mathrm{refl}_{S^1}(b), l):S^1 \times S^1 \to S^1$$ category: redirected to nlab