$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$ Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
This is impossible.

Suppose that we have such a type $T$, with an implementation of addition $\mathit{add} : T \to T \to T$, which is judgementally commutative.
Because MLTT is strongly normalising, we know that we can put $\mathit{add}$ in $\beta$-normal, $\eta$-long form.
Now suppose that we have two variables $x, y$ of type $T$.
Now consider the terms $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$.
Substituting $x$ and $y$ for the formal parameters of $\mathit{add}$ will not create any new $\beta$-reducible expressions, because $x$ and $y$ are neutral terms.
Now, $\eta$-expand the occurences of $x$ and $y$ as demanded by the definition of $T$.
Now, the resulting terms will be identical except that we've permuted the occurences of $x$ and $y$.
Recall that judgemental equality for $\beta$-normal, $\eta$-long terms is just $\alpha$-equivalence.
Since we assumed $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$ were assumed to be judgementally equal, this means that the normal forms for these two terms are $\alpha$-equivalent.
Since anywhere that $x$ occurs in the normal form for $\mathit{add}\,x\,y$, a $y$ occurs in the corresponding position of the normal form for $\mathit{add}\,y\,x$, the only way that these two terms can be $\alpha$-equivalent is if neither $x$ nor $y$ occurs in the term.
This means that $\mathit{add}\,x\,y$ and $\mathit{add}\,y\,x$ do not use their arguments!
As a result, we can conclude that $\mathit{add}\,1\,1$ and $\mathit{add}\,0\,0$ are also judgementally equal.
Therefore $T$ cannot be the natural numbers, since $2$ and $0$ must not be judgementally equal.