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

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)?

• Excuse a possibly silly question, but why is the assumption of consistency needed? Commented Mar 11, 2022 at 8:18
• What is the precise question here? In MLTT it is true that "if all closed terms of $\mathbb{N}$ have canonical forms then all closed terms have canonical forms" simply because "all closed terms have canonical forms" (for those types that have a reasonable notion of canonicity). Are you asking whether the implication holds more broadly for other type theories? Almost nothing is true more broadly for other type theories, because there are some pretty crazy ones. Please explain the context and the scope of the question a bit more. Commented Mar 11, 2022 at 8:21
• While you are at it, what is the canonical form of a term of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$? Strong normal form? Commented Mar 11, 2022 at 8:21
• @AndrejBauer Ahh... My bad. I don't think consistency is needed. I should have said that consistency is not a corollary of ℕ-canonicity and hence ought to be assumed additionally. Commented Mar 12, 2022 at 1:54
• It's vague because I'm not sure how to describe it more precisely. Maybe I should narrow things a bit. It makes more sense to talk about canonical form of an inductive type, so that a term is canonical if it composed solely of constructors and application of constructors. Commented Mar 12, 2022 at 1:59

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.
• You can always use a constant function in every "branch" as I did in the bool case, no matter how complex the inductive type. In Coq, you would do something like match s return nat with | c _ … _ => 0 | … end, the only issue being the number of underscores. Commented Mar 14, 2022 at 7:49