Does the canonicity of natural number imply that of all types?

Question

I've heard about a folklore claim that

If all terms of ℕ are literals, all closed terms admit canonical form.

In MLTT-style type theories.

I am assured that it's true for Bool if one also assumes consistency, namely the canonicity for empty type. Unfortunately, I don't know much about the general case, and couldn't find references. I suppose that it's related to encoding terms by natural numbers or something similar...

Does anyone know a rigorous formulation or a proof (or a disproof)?

Answer 1

Your question is quite vague, so let me give you both an intuition on why this ought to be true, and a counterexample.

As for intuition, let me show how supposing only canonicity for $\mathbb{N}$ (natural numbers) one can deduce canonicity for $\mathbb{B}$ (booleans). Suppose we are given a closed boolean $\vdash b : \mathbb{B}$, and consider $$\mathtt{if}~b~\mathtt{then}~0~\mathtt{else}~0$$ This is a natural number in the empty context, so it must reduce to a canonical form. But to do so it must be the case that $b$ also reduces to a canonical form, because this is the only way for the $\mathtt{if}$ statement to reduce!

Abstracting a bit, if we can construct a context $\vdash C[\cdot] : T \Rightarrow T'$, that is a term with a hole such that whenever a term $\vdash t : T$ is plugged in said hole the whole term is of type $T'$, and such that $C[t]$ has a canonical form only if $t$ has, then canonicity for $T'$ implies canonicity for $T$.

But there are perfectly valid cases where such a context cannot be built, and this is intentional! My favorite example is the sort of (proof-irrelevant) propositions $\mathtt{SProp}$. As shown in a recent article (and its predecessor), you can prove canonicity for natural numbers in MLTT extended with $\mathtt{SProp}$ without proving canonicity of inhabitants of strict propositions – you only have to assume consistency. The trick is to control the way one can use those to build relevant terms (in our case, natural numbers) so that no context like the above can be built. The idea is roughly to allow for an eliminator from $\mathtt{SProp}$ to $\mathbb{N}$ only for the false proposition. This ensures that a natural number in the empty context cannot be stuck on this eliminator since that would mean that one has an inconsistency in the theory – the term on which the eliminator is applied would be a proof of falsity in the empty context.