You proof strategy is valid, let's complete it.
Assume $a : \neg P \vdash n : \mathbb{N}$, ie we have a "closed" natural number $n$, but which uses axiom $a : \neg P$. By normalisation, we can assume that $n$ is in normal form. From the definition of normal forms at $\mathbb{N}$, there are two possibilities:
- either $n$ is a numeral $S^k(0)$, in which case we are done;
- otherwise, $n$ must be of the form $S^k(n')$ with $k$ an (external) natural number and $n'$ a neutral, let us show this case is impossible.
Neutrals always are of the shape $E[x]$ where:
- $x$ is a variable
- $E$ is an evaluation context, ie a (possibly empty) list of eliminations ($- t$, $π_i -$, $\mathrm{rec}_{\bot}(-,A)$, $\mathrm{rec}_{\mathbb{N}}(-,P,b_0,b_S)$, etc.)
Here the only variable in context is $a$, so $n'$ must be of the form $E[a]$ for some evaluation context $E$.
$E$ cannot be empty, because otherwise we would have $n' = a$ thus $a : \neg P \vdash a : \mathbb{N}$, and therefore $\vdash \neg P \equiv \mathbb{N}$, which is impossible by no-confusion of type constructors. Moreover, again because of typing constraints, the innermost elimination in $E$ must be an application, ie $n'$ must actually be of the shape $E[a~p]$ (if it was for instance a projection, we would have $\neg P \equiv \Sigma x : A.B$ for some $A$ and $B$, which is not possible, again because of no-confusion). Eliminations never bind variables, so $p$ lives in the same context as $n'$, and as an argument to $a$ must have type $P$.
We have obtained some $p$ such that $a : \neg P \vdash p : P$. Now we are almost done. First, we get $\vdash \lambda a. p : \neg P \to P$. But it is a theorem of MLTT that $(\neg P \to P) \to \neg \neg P$, for any type $P$. Thus, applying this to the above, we get that $\neg \neg P$ is derivable, thus $\neg P$ is not a consistent axiom, contradicting our hypothesis.
