3
$\begingroup$

We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics.

Now if we were to drop general $W$-types but keep just one $W$-type with infinitely many closed terms how much more difficult would our life become? Would it be much harder to express interesting theorems?

$\endgroup$
3
$\begingroup$

We certainly do not need very many $W$-types.

If we also have universes, we only need one $W$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no other inductive types (if we discount the fact that standard types constructors, such as products and sum, are defined inductively in Coq).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy