Adding a little to other good answers, especially Andrej’s: Nothing in this discussion is specific to Martin-Löf type theory. All these phenomena show up in other foundational systems, like ZFC or PA — and perhaps looking at them there may clarify them, for some readers.
In ZFC, for instance, you can of course prove “Every element of $\mathbb{N}$ is either zero or a successor” — this follows directly from induction for $\mathbb{N}$, and is often mentioned as part of the intuitive motivation for induction. But consider the number $\chi_{CH}$, defined to be 1 if the continuum hypothesis holds, and 0 if CH fails. Since CH is independent of ZFC, we know ZFC can’t prove either that $\chi_{CH} = 1$, or $\chi_{CH} = 0$. There’s no contradiction here, but it shows we have to distinguish between:
ZFC proves “every element of $\mathbb{N}$ is either zero or a successor”;
for every ZFC-definable element of $\mathbb{N}$, either ZFC proves it is 0, or ZFC proves it is a successor.
We’ve seen that for ZFC, (1) holds, quite easily and (2) fails, quite non-trivially. Similarly, with type theory, we can distinguish:
MLTT proves “every element of $\mathbb{N}$ is either zero or a successor”;
for every MLTT-term of type $\mathbb{N}$, either it is [provably or judgementally] equal to 0, or to a successor.
There are two differences in the phrasing: MLTT has a much richer term language, so we can say “term” instead of “definable element”; and MLTT has several different notions roughly corresponding to provable-equality in ZFC, each giving a different variant of (2). But again, (1) and the variants of (2) are very different: (1) holds, quite easily (again directly provable from the induction principle of $\mathbb{N}$\mathbb{N}$); while (2) may hold or fail depending which variant of it and which variant of MLTT you consider, but in any case it is a quite non-trivial property, and very distinct from (1).
