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

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.

• How much structure are you assuming, something like MLTT ($\Pi$, $\Sigma$, $\mathrm{Id}$, $\mathbb{N}$, $0$, $1$, $2$), possibly with universes? Commented Aug 23, 2022 at 6:22
• proofassistants.stackexchange.com/a/1377/153 apparently a generic construction is possible within simple type theory. However, I don't really understand the construction myself. Commented Aug 23, 2022 at 17:18
• @MolossusSpondee That answer there only seems to address HOL-like settings, but HOL importantly lacks dependency and universes, note the signature of W (A : Set) (B : A -> Set) : Set, in HOL type families like B cannot be defined (we could still quantify over small A).
– Ilk
Commented Aug 23, 2022 at 17:50
• yes, that's what I am trying to say is that intensional MLTT + N should be an internal language of locally closed cartesian categories with NNO, not topos with an NNO, so the quote would only apply to stronger type theories/internal languages and won't tell us much about the W-types in internal language of LCCC+NNO.
– Ilk
Commented Aug 25, 2022 at 4:44
• Wikipedia's page on ordinal analysis says that the proof theoretic ordinal for MLTT without W-types (but with universes) is smaller than that for MLTT with W-types (even without universes). So, that suggests that you cannot build W-types with just ℕ and (predicative) universes. It's not very clear where all the information on that page comes from, though. Commented Aug 28, 2022 at 23:19

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$$.