Recent work on higher-dimensional dependent type theory enriches conventional
one-dimensional dependent type theory with additional structure expressing
equivalence of elements of a type. This structure may be employed in a variety
of ways to capture rather coarse identifications of elements that must be
respected by type families. Higher-dimensional type theory has applications to
code reuse for dependently typed programming, and to the formalization of
mathematics. In this paper, we develop a novel judgemental formulation of a
two-dimensional type theory, which enjoys a canonicity property: a closed term
of boolean type is definitionally equal to one of the two booleans. Canonicity
is a necessary condition for a computational interpretation of type theory as a
programming language, and does not hold for existing axiomatic presentations of
higher-dimensional type theory. The method of proof is a generalization of the
NuPRL semantics, interpreting types as syntactic groupoids rather than
equivalence relations.