Minimal specification of Martin-Löf type theory

Question

I'm reading the formal presentation of Martin-Löfs type theory (appendix of the HoTT book). The authors introduce a hierarchy of universes, then $\Pi, \Sigma,+, {\bf 0}, {\bf 1}$ and also $W$-types as well as natural numbers $\mathbb N$ (inductively via $0$ and $succ$). Eventually they add higher inductive types too.

But then I wonder why it's necessary to do $\mathbb N$ in the theory specification. Doesn't ${\bf 1}$ and $+$ and algebraic data types, in the incarnation of having $W$-types, suffice to set it up? E.g. with the initial algebra approach. (Or at least after we pass from MLTT to HoTT have inductive types - after all, the integers $\mathbb Z$ emerge as homotopy group of circle type $\mathbb S$ within the theory.)

Or has it to do with our need to have primitive recursion from the start, which is defined right next to $\mathbb N$ in the presentation? This is an idea which I have because I don't quite know how "definition is defined" in that framework, or how extending the language works, formally. I might add that I recognize that at least an informal notion of numbers and "greater" is used already when the hierarchy of universes is defined.

In case one can spare $\mathbb N$ and the specification is just not minimal, are there other items one could, in principle, drop? E.g. I could imagine $\bf 2$ and then $+$ coming from some combination of $\Pi, \Sigma, {\bf 0}, {\bf 1}$, but I was not able to do it.

Answer 1

The purpose of the system described in the appendix of the HoTT book is to present something that corresponds to what is used by the book. The book is aiming to be educational. Therefore it would be a bad idea to do everything in a minimalist way. For example, we introduce $\mathbb{N}$ separately because it is instructional to see how inductive constructions work in a familiar case.

You are perfectly correct, to jump-start inductive types from general $W$-types you just need $0$ and $2$. You immediately get $1$ as $0 \to 0$, and you get $+$ from $2$ and $\Sigma$. Once you have that, you get all finite sums $1 + 1 + \cdots + 1$. At this point it is easy to do the usual algebraic datatypes.

If you drop $0$, so you start from $\Pi$, $\Sigma$, $1$ and $2$, then you cannot get $0$ back because every type you make will be inhabited.

Suppose you only have $\Pi$, $\Sigma$, $0$ and $1$. Then you cannot make $2$ because you can show that every construction you make gives you back either $0$ or $1$. In fact, you cannot make any interesting dependent families at all. A larger family of types which is closed under $\Pi$, $\Sigma$, $0$ and $1$, but does not contain $2$ is the $(-1)$-types (propositions).