[[!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. Or set theory or univalent universes for that matter. That is for the actual mathematicians to do, and I am just a logician. category: redirected to nlab