Contrary to previous belief, intensional type theory with W types as the only primitive inductive type is expressive enough to construct the natural numbers along with a whole host of inductive types.

Coq (version 8.12) sources are in code, LaTeX sources are in paper.