In laying down the equality rules in Martin-Löf type theory, e.g., for the type $\mathsf{N}$ of natural numbers, there seems to be an implicit assumption that any natural number is either $0$ or $S(a)$ for some $a\in\mathsf{N}$; in other words, only the so-called 'canonical' elements of the type $\mathsf{N}$ are given rules for their equality. Of course, we do know, from our background understanding of natural numbers and their inductive construction (as the smallest set such that …) that they are either $0$ or $S(a)$ for some $a$, but I wonder how this is granted by the rules of Martin-Löf type theory. The introduction rules only say that $0\in \mathsf{N}$ and that if $a\in \mathsf{N}$ then $S(a)\in \mathsf{N}$, but I don't see how this guarantees there's no other element in $\mathsf{N}$.
Is the assumption that any natural number is of one of its two canonical forms only implicitly assumed or is there a way we can derive it from the deductive rules that characterize $\mathsf{N}$? Is the fact that we're not laying down any other rule for introduction itself a way of carrying the idea? (A similar question applies to other types.)
Best Answer
There is no such implicit assumption at all. You are missing one rule for natural numbers, namely the induction principle. The rules for natural numbers are: $$\frac{}{\vdash \mathbb{N} \; \mathsf{type}} \qquad \frac{}{\vdash 0 : \mathbb{N}} \qquad \frac{\vdash t : \mathbb{N}}{\vdash \mathsf{S}(t) : \mathbb{N}} \\[4ex] \frac{n {:} \mathbb{N} \vdash P(n) \;\mathsf{type} \quad \vdash t : P(0) \quad n {:} \mathbb{N}, y {:} P(n) \vdash f : P(\mathsf{S}(n)) \quad \vdash e : \mathbb{N}}{\vdash \mathsf{rec}(t, (n \, y . f), e) : P(e)} $$ The last rule is the induction principle, stated type theoretically. The technical details are not too important, but briefly, $t$ is the base case and $f$ is the induction step. There are also further equations governing $\mathsf{rec}$, but they are not important for this discussion.
There is no mysterious, implicit, cultural, meta-level or other kind of hidden anything. The above rules are all there is to say about $\mathbb{N}$.
Now, using the induction principle we can derive an inhabitant of the type \begin{equation} \textstyle\prod (n : \mathbb{N}) \,.\, \left(\mathsf{Id}(n, 0) + \sum (m : \mathbb{N}) \,.\, \mathsf{Id}(n, \mathsf{S}(m)\right) \tag{1} \end{equation} This type says "every natural number is either 0 or a successor". I will leave this as an exercise, it's not hard.
A word of warning: sometimes people think of types as collections of terms (expressions), especially when their background is programming and computer science. From a mathematical point this is a bad idea, or at least as bad as thinking that a function is a symbolic expression (historically, this was the accepted understanding, and is quite natural for pre-college students), or that a surface is made of set-theoretic expressions denoting its points.
Anyhow, when people do think of type theory as a purely syntactic entity, then they might prove a meta-theorem that says something like "every closed term of type $\mathbb{N}$ is judgementally equal to one of the form $S(S(\cdots S(0)))$". Such theorems have their place and are important, but they do not say that every element of $\mathbb{N}$ is either 0 or a successor. Expressions are not the inhabitants of a type, they are just representations of some of the inhabitants. Depending on a model, there may be others.
In your question you state that we "know" that every natural number is zero or a successor because we construct $\mathbb{N}$ as "the smallest set such ..." True, taking such a smallest set is a method of ensuring that the induction principle will be validated - and the induction principle then implies the statement "every number is $0$ or a successor".
But taking "the smallest set such ..." is not a method of insuring that the set will only contain elements of the form $S(S(...S(0)))$! For if you carry out the construction in a non-standard model of set theory, you will get non-standard natural numbers which are not denoted by any expression of the form $S(S(...S(0)))$. And in a Boolean topos such as $\mathsf{Set}^2$, the construction will produce what we would view as $\mathbb{N} \times \mathbb{N}$. It is still true inside the model that "every number is zero or a successor" – and that corresponds precisely to the fact that inside type theory (1) is inhabited.
I am not sure all of this is making things clearer, but I hope it at least points to some possible misunderstandings.