First, we should pin down that we're talking about closed terms with natural number type, that is, terms without free variables. A free variable with type $\mathsf{N}$ is clearly not of the form $0$ or $S(n)$.

A type theory has the canonicity property if all closed terms with type $\mathsf{N}$ are definitionally equal to a numeral, i.e. a finite successor of $0$.

This property is not an assumption. It is a provable property for most commonly used type theories, which follows from the specification of the theory. It is not enough though to only look at the rules for natural numbers, we have to consider all rules of a type theory simultaneously, because (intuitively) it is possible to construct numbers from various other types. For example, if we add the law of excluded middle as an axiom, that makes canonicity fail, since it introduces non-constructive definitions which cannot be computed to numerals.

Canonicity proofs are moderately complex for interesting type theories. The easiest way is to do "proof-relevant logical predicates", or "Artin gluing". Sterling - Algebraic Type Theory and Universe Hierarchies is a fairly accessible and detailed exposition. In a nutshell, we construct the following by induction on the syntax of a theory:

• For each typing context, a family of sets indexed by parallel substitutions targeting the context (a "proof-relevant predicate").
• For each type in a context, a family of sets indexed by terms of the type.
• For each parallel substitution, a function which witnesses that the substitution preserves predicates.
• For each term, again a function witnessing preservation of predicates.

Concretely for the $\mathsf{N}$ type, we may pick the predicate which says that a given term is a numeral. Then, from the above induction, and also from the fact that the predicate corresponding to the empty context is trivially true, we get that every closed term with type $\mathsf{N}$ must be a numeral.

First, we should pin down that we're talking about closed terms with natural number type, that is, terms without free variables. A free variable with type $\mathsf{N}$ is clearly not of the form $0$ or $S(n)$.

A type theory has the canonicity property if all closed terms with type $\mathsf{N}$ can be computed to a numeral, i.e. a finite successor of $0$.

This property is not an assumption. It is a provable property for most commonly used type theories, which follows from the specification of the theory. It is not enough though to only look at the rules for natural numbers, we have to consider all rules of a type theory simultaneously, because (intuitively) it is possible to construct numbers from various other types. For example, if we add the law of excluded middle as an axiom, that makes canonicity fail, since it introduces non-constructive definitions which cannot be computed to numerals.

Canonicity proofs are moderately complex for interesting type theories. The easiest way is to do "proof-relevant logical predicates", or "Artin gluing". Sterling - Algebraic Type Theory and Universe Hierarchies is a fairly accessible and detailed exposition. In a nutshell, we construct the following by induction on the syntax of a theory:

• For each typing context, a family of sets indexed by parallel substitutions targeting the context (a "proof-relevant predicate").
• For each type in a context, a family of sets indexed by terms of the type.
• For each parallel substitution, a function which witnesses that the substitution preserves predicates.
• For each term, again a function witnessing preservation of predicates.

Concretely for the $\mathsf{N}$ type, we may pick the predicate which says that a given term is a numeral. Then, from the above induction, and also from the fact that the predicate corresponding to the empty context is trivially true, we get that every closed term with type $\mathsf{N}$ must be a numeral.

First, we should pin down that we're talking about closed terms with natural number type, that is, terms without free variables. A free variable with type $\mathsf{N}$ is clearly not of the form $0$ or $S(n)$.

A type theory has the canonicity property if all closed terms with type $\mathsf{N}$ are definitionally equal to a numeral, i.e. a finite successor of $0$.

This property is not an assumption. It is a provable property for most commonly used type theories, which follows from the specification of the theory. It is not enough though to only look at the rules for natural numbers, we have to consider all rules of a type theory simultaneously, because (intuitively) it is possible to construct numbers from various other types. For example, if we add the law of excluded middle as an axiom, that makes canonicity fail, since it introduces non-constructive definitions which cannot be computed to numerals.

Canonicity proofs are moderately complex for interesting type theories. The easiest way is to do "proof-relevant logical predicates", or "Artin gluing". This is a fairly accessible and detailed exposition. In a nutshell, we construct the following by induction on the syntax of a theory:

• For each typing context, a family of sets indexed by parallel substitutions targeting the context (a "proof-relevant predicate").
• For each type in a context, a family of sets indexed by terms of the type.
• For each parallel substitution, a function which witnesses that the substitution preserves predicates.
• For each term, again a function witnessing preservation of predicates.

Concretely for the $\mathsf{N}$ type, we may pick the predicate which says that a given term is a numeral. Then, from the above induction, and also from the fact that the predicate corresponding to the empty context is trivially true, we get that every closed term with type $\mathsf{N}$ must be a numeral.

First, we should pin down that we're talking about closed terms with natural number type, that is, terms without free variables. A free variable with type $\mathsf{N}$ is clearly not of the form $0$ or $S(n)$.

A type theory has the canonicity property if all closed terms with type $\mathsf{N}$ are definitionally equal to a numeral, i.e. a finite successor of $0$.

This property is not an assumption. It is a provable property for most commonly used type theories, which follows from the specification of the theory. It is not enough though to only look at the rules for natural numbers, we have to consider all rules of a type theory simultaneously, because (intuitively) it is possible to construct numbers from various other types. For example, if we add the law of excluded middle as an axiom, that makes canonicity fail, since it introduces non-constructive definitions which cannot be computed to numerals.

Canonicity proofs are moderately complex for interesting type theories. The easiest way is to do "proof-relevant logical predicates", or "Artin gluing". Sterling - Algebraic Type Theory and Universe Hierarchies is a fairly accessible and detailed exposition. In a nutshell, we construct the following by induction on the syntax of a theory:

• For each typing context, a family of sets indexed by parallel substitutions targeting the context (a "proof-relevant predicate").
• For each type in a context, a family of sets indexed by terms of the type.
• For each parallel substitution, a function which witnesses that the substitution preserves predicates.
• For each term, again a function witnessing preservation of predicates.

Concretely for the $\mathsf{N}$ type, we may pick the predicate which says that a given term is a numeral. Then, from the above induction, and also from the fact that the predicate corresponding to the empty context is trivially true, we get that every closed term with type $\mathsf{N}$ must be a numeral.