$\def\opn{\operatorname}$
$\def\mb{\mathbb}$
To prove this result, we shall define the observational equality principle for $\mb{N}$.
The observational equality $\opn{Eq}_{\mb{N}} : \mb{N} \rightarrow \mb{N} \rightarrow \mathcal{U}$ satisfies the following equations :
\begin{align}
\opn{Eq}_{\mb{N}}(0_\mb{N},0_\mb{N}) &:\equiv \mathbf{1} & \opn{Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n), 0_{\mb{N}}) &:\equiv \emptyset \\
\opn{Eq}_{\mb{N}}(0_{\mb{N}}, \opn{succ}_{\mb{N}}(n)) &:\equiv \emptyset & \opn{Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n),\opn{succ}_{\mb{N}}(m)) &:\equiv \opn{Eq}_{\mb{N}}(n, m)
\end{align}
Please note that it is also an inductive type :
\begin{align}
\opn{Eq}_{\mb{N}}(0_{\mb{N}}, m) &:\equiv \opn{E}_0(m) \\
\opn{Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n), m) &:\equiv \opn{E}_S(n, \opn{Eq}_{\mb{N}}(n), m)
\end{align}
with $\opn{E}_0 : \mb{N} \rightarrow \mathcal{U}$ being defined as
\begin{align}
\opn{E}_0(0_{\mb{N}}) &:\equiv \mathbf{1} \\
\opn{E}_0(\opn{succ}_{\mb{N}}(n)) &:\equiv \emptyset
\end{align}
and $\opn{E}_s$ defined as
\begin{align}
\opn{Eq}_S(n, X, 0_{\mb{N}}) &:\equiv \emptyset \\
\opn{Eq}_S(n, X, \opn{succ}_{\mb{N}}(m)) &:\equiv X(m)
\end{align}
This observational equality of the natural numbers is important because it can be used to prove equalities and inequalities.
The reflexive property of this relation, enables us to do so
$$\opn{refl-Eq}_{\mb{N}} : \prod_{n:\mb{N}} \opn{Eq}_{\mb{N}}(n, n)$$
which is again defined by induction on $\mb{N}$
\begin{align}
\opn{refl-Eq}_{\mb{N}}(0) &:\equiv \star \\
\opn{refl-Eq}_{\mb{N}}(\opn{succ}_{\mb{N}}(n)) &:\equiv \opn{refl-Eq}_{\mb{N}}(n)
\end{align}
Giving this definition, we can easily prove by induction that for $m, n : \mb{N}$
$$(m = n) \iff \opn{Eq}_{\mb{N}}(m, n)$$
Hence, it follows there is a type family $$(0_{\mb{N}} = n) \rightarrow \opn{Eq}_{\mb{N}}(0_{\mb{N}}, n)$$ indexed by $n : \mb{N}$. Thus, since $\opn{Eq}_{\mb{N}}(0_{\mb{N}}, \opn{succ}_{\mb{N}}(n)) :\equiv \emptyset$ we have $$(0_\mb{N} = \opn{succ}_{\mb{N}}(n)) \rightarrow \emptyset$$
In an informal sense, the answer "should be yes", in the sense that if one ignore type theory and work with an $\infty$-topos one can make sense of the construction $List(A)$ either by the usual universal property of list objects or as $List(A) = \coprod_\mathbb{N} A^n$ (both definitions can be shown to be equivalent) and $List(A)$ is indeed the free $A_\infty$-algebra on $A$.
However, the big problem is that we don't even know how to phrase the precise question you are asking in terms of Homotopy type theory, and it is not possible to make sense of what I just said (at least at the present time) within homotopy type theory. The problem is that we do not know how to define what is an $A_\infty$-algebra within homotopy type theory. Being able to talk about this type of higher algebraic structure in HoTT, or show that it is impossible in some precise sense, is one of the biggest open problem in HoTT.
There are extensions of HoTT (like cubical HoTT, or maybe the simplicial HoTT of Riehl and Shulman with some additional work) that can/should be able to talk about higher structures like $A_\infty$-algebras, and where this problem might have a solution, but I don't think it has been worked out in details.
The best one might hope to do in standard "book HoTT" (at least with present technology) is for each external (that is metatheoretical) integer $n$, define what is an $n$-truncated $A_\infty$-algebra and show that for an $n$-truncated type, $List(A)$ is the free $n$-truncated $A_\infty$-algebra on the type $A$. I even suspect we would only know how to do this for small values of $n$, though I might be wrong.
Best Answer
Daniel's answer is correct that the judgmental distinctness of $0$ and $\mathsf{succ}(m)$ is not what justifies a definition by pattern-matching. However, it is still a meaningful question of how to prove that $0$ and $\mathsf{succ}(m)$ are not judgmentally equal. (Stretching terminology a bit, Daniel answered your X and I'm going to answer your Y.)
Note that this is a metatheoretic question, in contrast to the internal proof that $0\neq \mathsf{succ}(m)$. Thus, even though judgmental equality implies typal equality, the answer to that question does not answer this one.
It's also worth noting that this is not a trivial question, even though $0$ and $\mathsf{succ}$ are distinct constructors. From an "algebraic" perspective on type theory, judgmental equality is just the smallest congruence generated by certain rules. Thus, two terms that don't "look" like they could possibly be equal might turn out to be equal by passing through some chain of forwards and backwards equalities to other terms.
For the same reason, it is a "global" question about the type theory, not one that can be answered by referring only to $\mathbb{N}$. For instance, in a higher inductive type such as the interval $\mathsf{I}$, with constructors $\mathsf{zero},\mathsf{one} : \mathsf{I}$ and $\mathsf{seg}:\mathsf{zero}=\mathsf{one}$, there is no "local" reason for $\mathsf{zero}$ and $\mathsf{one}$ to be judgmentally equal; but if the type theory also includes the equality reflection rule, then $\mathsf{seg}$ implies that $\mathsf{zero}\equiv\mathsf{one}$.
One answer to this question involves giving an algorithm for checking whether two terms are judgmentally equal. Probably the simplest such algorithm involves giving a "rewriting system" under which every term can be reduced to a "normal form", and then two terms are judgmentally equal if they reduce to the same normal form (up to $\alpha$-equivalence). Roughly speaking, this rewriting system consists of what the HoTT Book calls "computation rules". One then has to prove that this rewriting system is terminating, and that the relation of "reducing to the same normal form" is a congruence; thus it coincides with judgmental equality. Then one can simply observe that $0$ and $\mathsf{succ}(m)$ are (when $m$ is a variable) distinct normal forms.
In practice, nowadays more complicated algorithms are used. Among other reasons, this is in order to also include what the HoTT Book calls "uniqueness rules". These algorithms often go by names like "normalization by evaluation". The crucial idea is that there are two "phases" of the algorithm, one which applies the computational rewrites, and another which applies the uniqueness rules in the expansionary direction ($f \mapsto (\lambda x. f(x))$ or $u \mapsto (\pi_1(u),\pi_2(u))$) by inspecting their types. But the basic idea is the same: after proving that the algorithm is terminating and complete, we can run the algorithm on two terms to verify that they are unequal (or equal).
With that said, I don't know whether anyone has actually done this for Book HoTT. It's known for MLTT, on which Book HoTT is based, but Book HoTT adds not just axioms (which don't disrupt such an algorithm) to MLTT but new judgmental equalities (the computation rules for point-constructors of HITs), which then have to be incorporated in the algorithm. So (even laying aside the point that "Book HoTT" is not precisely specified because it is open-ended with respect to what HITs are definable) there may technically be an open question here. However, I think no type theorist who's familiar with such proofs would have much doubt that standard techniques ought to apply to Book HoTT (and it's possible that someone has already done it).
Edit: Simon has pointed out in the comments what I should clearly have realized myself, namely that another way to deduce that two terms are not judgmentally equal is to give a model in which they are interpreted by distinct things. Thus, for instance, the set-theoretic model proves this for MLTT, and the simplicial set model proves it for Book HoTT (modulo details in the construction of that model that aren't yet in the literature, such as showing that the univalent universes are closed under a sufficiently large class of higher inductive types).