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).
Here is an alternative proof based on Russell's paradox rather than cardinality that doesn't require sets cover, although I do need to assume that hom sets are 0 truncated. The rough outline is to modify Gylterud's definition of the cumulative hierarchy by limiting it to sets that can be constructed from $\mathcal{C}$ to make it a small type, and then follow the usual proof of Russell's paradox.
The first step is the following lemma.
Lemma There is a small type $X : \mathcal{U}$ together with an embedding $\iota : X \hookrightarrow \mathcal{U}$ such that every type that can be expressed as a set quotient of a subtype of a type of the form $\mathcal{C}(a, b)$ for $a, b : \mathcal{C}_0$, is equivalent to one in the image of $\iota$.
Proof For each $a, b : \mathcal{C}_0$ we can express every subobject $Z \hookrightarrow \mathcal{C}(a, b)$ of $\mathcal{C}(a, b)$ as $\sum_{f : \mathcal{C}(a, b)} \chi(f) = 1$ for some map $\chi: \mathcal{C}(a, b) \to 2$. Furthermore, every set quotient of $Z$ is the quotient of some equivalence relation $R : Z \times Z \to 2$. This gives a type $Y$ together with a map $Y \to \mathcal{U}$ whose image contains every set quotient of every subtype of $\mathcal{C}(a, b)$ for every $a, b : \mathcal{C}_0$. By type theoretic replacement (Theorem 4.6 in Rijke, The join construction), we can take the image of this map to be small type, which is the required $X$.$\quad \square$
Next we construct a modified version of the Aczel cumulative hierarchy $M$ as the $W$-type with constructors $X$, and the arity of $x : X$ is just $\iota(x)$. Note that since $X$ is a small type, and all the arities are small, so is $M$, unlike the usual Aczel hierarchy. We then construct a retract of $M$ corresponding to the construction of the HIT cumulative hierarchy in Gylteud, From multisets to sets in homotopy type theory. Namely an element of $M$ of the form $\sup(x, \alpha)$ for $x : X$ and $\alpha : \iota(x) \to M$ is a hereditary embedding if $\alpha$ is an embedding and $\alpha(y)$ is a hereditary embedding for all $y : \iota(x)$. Write $V$ for the subtype of $M$ consisting of hereditary embeddings. Since $V$ is a subtype of $M$, it is also small. Following the same argument that Gylterud used for the cumulative hierarchy (section 5 of paper above), $V$ is necessarily 0-truncated. We define membership $\in$ the same as Gylterud does.
Now suppose that we are given $f \neq g : \mathcal{C}(a, b)$. Define $c$ to be the product $\prod_V b$. We have injections $V \hookrightarrow 2^V \hookrightarrow \mathcal{C}(a, c)$. Since $V$ and $\mathcal{C}(a, c)$ are both sets, this gives us a surjection $s : \mathcal{C}(a, c) \twoheadrightarrow V$. We define a subtype $Z$ of $V$ as $Z := \sum_{z : V} z \notin z$. Pulling back along $s$ gives us a subtype $Z'$ of $\mathcal{C}(a, c)$ together with a surjection $Z' \twoheadrightarrow Z$. Since $Z'$ and $Z$ are both sets, $Z$ must be a set quotient of $Z'$. Hence $Z$ is equivalent to $\iota(x)$ for some $x$. Hence we have $z_0 : V$ such that for all $z \in z_0 \;\simeq\; z \notin z$ for all $z : V$, which gives a contradiction by Russell's paradox.
Best Answer
$\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$$