Can you build W-types out of natural numbers predicatively?

Question

I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, potentially giving up some of the judgmental equalities, but keeping the propositional equality the same? I always thought it was the case based on this quote from nLab W-type page:

"In a topos with a natural numbers object (NNO), W-types for any polynomial endofunctor can be constructed as certain sets of well-founded trees; thus every topos with a NNO is a ΠW-pretopos. This applies in particular in the topos Set (unless one is a predicativist, in which case Set is not a topos and W-types in it must be postulated explicitly)."

But I am unsure if this is a correct interpretation of the categorical concepts involved. I think the culprit here is the requirement of a topos with NNO, not just a locally cartesian closed category. Is this the case? Can we construct W-types from natural numbers?

Edit: I have found a construction of W-types from natural numbers in presence of propositional resizing in Strictly Positive Types in Homotopy Type Theory, so I think I should specify that I want to keep the theory as predicative as possible and hopefully free of uses of K or univalence.

Edit 2: To specify what I mean by intensional MLTT, it is the rules for $\Pi$, $\Sigma$, $\mathbb{N}$, Id, 0, 1, 2, plus an infinite predicative hierarchy of universes. $U_0 : U_1$, $U_1 : U_2$ etc.

Answer 1

The answer is no. According to Anton Setzer's PhD thesis: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe:

Aczel has shown in [Acz77] that Martin-Löf’s type theory with one universe but no W-type has strength $| \widehat{ID}_1 | = \phi_{\epsilon_0}0$.

However:

The strength we prove, is in fact far bigger [than that shown by Palmgren], it is slightly bigger than the strength of $| KP_i|$. Until recently (work of Rathjen, [Rat90], [Rat91a], [Rat92], see also [Buc93], [Sch91a], [Sch91b], [Sch92b]), $KP_i$ has been essentially the strongest theory, for which proof theoretical analysis could be carried out. For the author, $|KP_i|$ is an ordinal which seems to be an ordinal of significance similar to that of $\Gamma_0$

Furthermore:

Precisely we calculate the proof theoretical strength of intensional Russel, extensional, Tarski, and extensional Russel-version of Martin-Löf’s type theory with one Universe and the W-type, $ML^i_1W_R$ , $ML^e_1W_T$ and $ML^e_1 W_R$, namely $$|ML^i_1W_R| =|ML^e_1W_T|=|ML^e_1 W_R|= |\bigcup_{n\in{\mathbb N}}KPi_n^+| = \psi_{\Omega_1}\Omega_{I+\omega}.$$

This sorts out the proof theoretical strength for MLTT with a single universe.

Now, according to Michael Rathjen's paper The strength of Martin-Löf type theory with a superuniverse (which is at least stronger than MLTT with an infinite hierarchy of universes):

the proof-theoretic ordinal of $MLS$ is $\Phi_{\Gamma_0}0$

But according to the wikipedia page on ordinal analysis, as pointed out by Dan Doel, $$\phi_{\epsilon_0}0 < \Gamma_0 < \Phi_{\Gamma_0}0 < \psi_{\Omega_1}\Omega_{I+\omega}$$

And therefore $|ML_\omega| < |ML_1W|$ thus it cannot be possible to encode W-types in $ML_\omega$.