[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Primitive recursive arithmetic means that I am entirely wrong about the nature of the natural numbers. The natural numbers can be defined predicatively without universal quantifiers. * Wikipedia, [Primitive recursive arithmetic](https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic) Primitive recursive arithmetic to define the natural numbers finitely without logic, then define the universe hierarchy of book HoTT using the numbers in primitive recursive arithmetic. There is no need to define a separate proposition judgment, only universe level judgments and typing judgments. Every type is an element of a Russell universe. The end of strong predicativity. The natural numbers come first, and then types/sets/whatever come afterwards. ---- I don't care about number theory or real analysis anymore. That is for the actual mathematicians to do, and I am just a logician. ---- IZF defined without propositional truncations. Everything is structure... We define set theory in dependent type theory: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash V \; \mathrm{type}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:V, y:V \vdash x \in y \; \mathrm{type}}$$ $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{proptrunc}:\prod_{x:V} \prod_{y:V} \mathrm{isProp}(x \in y)}$$ $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ext}_V:\prod_{x:V} \prod_{y:V} (x =_V y) \simeq \prod_{z:V} (z \in x) \simeq (z \in y)}$$ $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{union}_V:\prod_{x:V} \sum_{U:V} \prod_{y:V} \prod_{z:V} (y \in x) \times (z \in y) \to (z \in U)}$$ $$\frac{\Gamma, x:V \vdash \phi(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{seperation}_V(x:V.\phi(x)):\left(\prod_{x:V} \mathrm{isProp}(\phi(x))\right) \to \prod_{a:V} \sum_{S:V} \prod_{x:V} (x \in a) \to (\phi(x) \simeq (x \in S))}$$ $$\frac{\Gamma, x:V, y:V \vdash \phi(x, y) \; \mathrm{type}}{\Gamma \vdash \mathrm{collection}_V(x:V.y:V.\phi(x, y):\left(\prod_{x:V} \prod_{y:V} \mathrm{isProp}(\phi(x, y))\right) \to \prod_{a:V} \left(\prod_{x:V} (x \in a) \to \sum_{y:V} \phi(x, y)\right) \to \sum_{b:V} \left(\prod_{x:V} (x \in a) \to \sum_{y:V} (y \in b) \to \phi(x, y)\right) \times \left(\prod_{y:V} (y \in b) \to \sum_{x:V} (x \in a) \to \phi(x, y)\right)}$$ category: redirected to nlab