A.4 Basic metatheory

This section discusses the meta-theoretic properties of the type theory presented insec: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 asan extension of the untyped $\lambda$-calculus. The $\lambda$-calculushas 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 formrewriting rules that determine reduction steps for a rewritingsystem. These steps yield a notion of computation in the sense that each rulehas a natural direction: one simplifies $(\lambda x.t)(u)$ by evaluating thefunction at its argument.

Moreover, this system is confluent, that is, if $a$ simplifies in somenumber 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 therewe presented the computation rules as undirected equalities $\equiv$, we can givean operational semantics by saying that the application of an eliminator to anintroductory form simplifies to its equal, not the other way around.)

It is straightforward to show that the system in sec:syntax-informallyhas 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, stronglynormalizable)if some (respectively, every), sequence of rewriting steps from the termterminates.

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 formif it cannot be furthersimplified, and that a term is closedif no variable occurs freely init. 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 closednormal terms may be omitted if empty, for instance, as with $\mathbb{N}$). In fact, wecan 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 thejudgment $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) followsimmediately: if we had $a:\mathrm{𝟎}$ in the empty context, then bythm:conversion-preserves-typing,thm:strong-normalization, $a$simplifies to a normal term $a^{\prime }:\mathrm{𝟎}$. But bylem: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 emptycontext, 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$; inother words, because type-checking amounts to verifying the correctness of aproof, 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 typetheory (i.e., the above system extended by sec:hott-features), sinceoccurrences of the univalence axiom and constructors of higher inductive typesnever simplify, breaking lem:normal-forms. It is an open questionwhether one can simplify applications of these constants in order to restorecanonicity. We also do not have a schema describing all permissible higherinductive types, nor are we certain how to correctly formulate their rules(e.g., whether the computation rules on higher constructors should be judgmentalequalities).

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

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