\begin{abstract}
Formal constructive type theory has proved to be an effective
language for mechanized proof. By avoiding non-constructive
principles, such as the law of the excluded middle, type theory
admits sharper proofs and broader interpretations of results. From
a computer science perspective, interest in type theory arises from
its applications to programming languages. Standard constructive
type theories used in mechanization admit computational
interpretations based on meta-mathematical normalization theorems.
These proofs are notoriously brittle; any change to the theory
potentially invalidates its computational meaning. As a case in
point, Voevodsky's univalence axiom raises questions about the
computational meaning of proofs.
We consider the question: \emph{Can higher-dimensional type theory
be construed as a programming language?} We answer this question
affirmatively by providing a direct, deterministic operational
interpretation for a representative higher-dimensional dependent
type theory with higher inductive types and an instance of
univalence. Rather than being a formal type theory defined by
rules, it is instead a computational type theory in the sense of
Martin-L\"{o}f's meaning explanations and of the NuPRL semantics.
The definition of the type theory starts with programs; types are
specifications of program behavior. The main result is a
canonicity theorem stating that closed programs of boolean type
evaluate to true or false.
\end{abstract}