[SabrinaJewson]

> 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 Ω).

[gugagore]

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.

[SabrinaJewson]

You need some source of infinite-ness, otherwise the entire theory can be modelled by finite sets. It can be provided by the natural numbers or W types or inductive types, but the naturals are arguably the most fundamental of the three.