A.4 Basic metatheory

This section discusses the meta-theoretic properties of the type theory presented in sec:syntax-informally, and similar results hold for sec:syntax-more-formally. Figuring out which of these still hold when we add the features from sec:hott-features quickly leads to open questions, as discussed at the end of this section.

Recall that sec:syntax-informally defines the terms of type theory as an extension of the untyped $\lambda$-calculus. The $\lambda$-calculus has its own notion of computation, namely the computation rule:

$$(\lambda x.t)(u):\equiv t[u/x]$$

This rule, together with the defining equations for the defined constants form rewriting rules that determine reduction steps for a rewriting system. These steps yield a notion of computation in the sense that each rule has a natural direction: one simplifies $(\lambda x.t)(u)$ by evaluating the function at its argument.

Moreover, this system is confluent, that is, if $a$ simplifies in some number of steps to both $a^{\prime }$ and $a^{\prime \prime }$, there is some $b$ to which both $a^{\prime }$ and $a^{\prime \prime }$ eventually simplify. Thus we can define $t\downarrow u$ to mean that $t$ and $u$ simplify to the same term.

(The situation is similar in sec:syntax-more-formally: Although there we presented the computation rules as undirected equalities $\equiv$, we can give an operational semantics by saying that the application of an eliminator to an introductory form simplifies to its equal, not the other way around.)

It is straightforward to show that the system in sec:syntax-informally has the following properties:

Theorem 12.5.1.

If $A\mathrm{:}\mathrm{U}$ and $A\mathrm{\downarrow }{A}^{\mathrm{\prime }}$ then $A^{\mathrm{\prime }}\mathrm{:}\mathrm{U}$. If $t\mathrm{:}A$ and $t\mathrm{\downarrow }{t}^{\mathrm{\prime }}$ then $t^{\mathrm{\prime }}\mathrm{:}A$.

We say that a term is normalizable (respectively, strongly normalizable) if some (respectively, every), sequence of rewriting steps from the term terminates.

Theorem 12.5.2.

If $A\mathrm{:}\mathrm{U}$ then $A$ is strongly normalizable. If $t\mathrm{:}A$ then $A$ and $t$ are strongly normalizable.

We say that a term is in normal form if it cannot be further simplified, and that a term is closed if no variable occurs freely in it. A closed normal type has to be a primitive type, i.e., of the form $c(\overrightarrow{v})$ for some primitive constant $c$ (where the list $\overrightarrow{v}$ of closed normal terms may be omitted if empty, for instance, as with $\mathbb{N}$). In fact, we can explicitly describe all normal forms:

Lemma 12.5.3.

The terms in normal form can be described by the following syntax:

$v$ $::=k\mid \lambda x.v\mid c(\overrightarrow{v})\mid f(\overrightarrow{v}),$

$k$ $::=x\mid k(v)\mid f(\overrightarrow{v})(k),$

where $f\mathit{}\mathrm{(}\overrightarrow{v}\mathrm{)}$ represents a partial application of the defined function $f$. In particular, a type in normal form is of the form $k$ or $c\mathit{}\mathrm{(}\overrightarrow{v}\mathrm{)}$.

Theorem 12.5.4.

If $A$ is in normal form then the judgment $A\mathrm{:}\mathrm{U}$ is decidable. If $A\mathrm{:}\mathrm{U}$ and $t$ is in normal form then the judgment $t\mathrm{:}A$ is decidable.

Logical consistency (of the system in sec:syntax-informally) follows immediately: if we had $a:\mathrm{𝟎}$ in the empty context, then by thm:conversion-preserves-typing,thm:strong-normalization, $a$ simplifies to a normal term $a^{\prime }:\mathrm{𝟎}$. But by lem:normal-forms no such term exists.

Corollary 12.5.5.

The system in sec:syntax-informally is logically consistent.

Similarly, we have the canonicity property that if $a:\mathbb{N}$ in the empty context, then $a$ simplifies to a normal term ${\mathrm{𝗌𝗎𝖼𝖼}}^k(0)$ for some numeral $k$.

Corollary 12.5.6.

The system in sec:syntax-informally has the canonicity property.

Finally, if $a,A$ are in normal form, it is decidable whether $a:A$; in other words, because type-checking amounts to verifying the correctness of a proof, this means we can always “recognize a correct proof when we see one.”

Corollary 12.5.7.

The property of being a proof in the system in sec:syntax-informally is decidable.

The above results do not apply to the extended system of homotopy type theory (i.e., the above system extended by sec:hott-features), since occurrences of the univalence axiom and constructors of higher inductive types never simplify, breaking lem:normal-forms. It is an open question whether one can simplify applications of these constants in order to restore canonicity. We also do not have a schema describing all permissible higher inductive types, nor are we certain how to correctly formulate their rules (e.g., whether the computation rules on higher constructors should be judgmental equalities).

The consistency of Martin-Löf type theory extended with univalence and higher inductive types could be shown by inventing an appropriate normalization procedure, but currently the only proofs that these systems are consistent are via semantic models—for univalence, a model in Kan complexes due to Voevodsky [klv:ssetmodel], and for higher inductive types, a model due to Lumsdaine and Shulman [ls:hits].

Other metatheoretic issues, and a summary of our current results, are discussed in greater length in the “Constructivity” and “Open problems” sections of the introduction to this book.

Title	A.4 Basic metatheory