Comment by SabrinaJewson
Comment by SabrinaJewson 3 days ago
> Is there anything more primitive than the inductive data type?
I believe that the natural numbers are more primitive than inductive data types, since all inductive data types may be constructed from the natural numbers alongside a small number of primitive type formers (e.g. Π, Σ, = and Ω).
You don't need all the natural numbers for that, though. I think you need 0 and 1 only?
I think there are two primitive sets for dependent type theory. The one with omega, and then the one with inductive types. None of them need axioms like the Peano axioms.