[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Type theory (dependent function types, dependent sum types, identity types, function extensionality) -> Predicate logic -> Set theory -> Number theory The free pointed type on a type: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A + 1 \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash \mathrm{in}_{A + 1}(x):A + 1 \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{pt}_{A + 1}:A + 1 \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A + 1 \vdash C(x) \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{in}_{A + 1}(x)) \quad \Gamma \vdash p:C(\mathrm{pt}_{A + 1})}{\Gamma, x:A + 1 \vdash \mathrm{ind}_{A + 1}^{C(-), c(-)}(p, x):C(x)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A + 1 \vdash C(x) \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{in}_{A + 1}(x)) \quad \Gamma \vdash p:C(\mathrm{pt}_{A + 1})}{\Gamma, x:A \vdash \mathrm{ind}_{A + 1}^{C(-), c(-)}(p, \mathrm{in}_{A + 1}(x)) \equiv c(x):C(\mathrm{in}_{A + 1}(x))}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A + 1 \vdash C(x) \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{in}_{A + 1}(x)) \quad \Gamma \vdash p:C(\mathrm{pt}_{A + 1}) }{\Gamma \vdash \mathrm{ind}_{A + 1}^{C(-), c(-)}(p, \mathrm{pt}_{A + 1}) \equiv p:C(\mathrm{pt}_{A + 1})}$$ The natural numbers type as the initial algebra on the free pointed type functor $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}$$ $$\frac{\Gamma \; \mathrm{type}}{\Gamma, x:\mathbb{N} + 1 \vdash \mathrm{zs}(x):\mathbb{N} \; \mathrm{type}}$$ ... category: redirected to nlab