Intuitionistic type theory as conceived by Martin-L\"{o}f in
fulfillment of Brouwer's foundational program is a comprehensive
theory of constructions intended as a framework for constructive
mathematics and computer programming. In its most widely used form
intuitionistic type theory is given by a formal system whose typehood
and membership judgments are inductively defined by a collection of
inference rules that circumscribe the theory. It is, as such, a theory
of formal proof, which lends itself immediately to implementation on a
computer as an aid to the discovery and verification of mathematical
arguments.

Computational type theory as conceived by Constable has a similar
intent, but with a rather different formulation. Rather than a theory
of proof, computational type theory is instead a Brouwerian account of
truth in mathematics that is based on the concept of a program. Types
and members are programs satisfying a collection of criteria, known as
a meaning explanation, that is intentionally open-ended, rather than
precisely circumscribed.  By starting with the notion of program
computational type theory is more directly in line with Brouwer's
ideas, and is directly applicable to the needs of computer science.

The concept of equality has been a source of difficulty for formal
type theory because it lacks a convenient way to express
extensionality equality of functions, or to support standard
mathematical ideas such as quotients.  To correct this homotopy type
theory has been proposed as an extension of formal type theory in
which the concept of equality is formulated in a proof-relevant manner
as a path in an abstract space, allowing for a richer conception than
has been hitherto feasible in that setting.  However, the
computational meaning for this theory seems elusive, and it appears
that frequent manipulation of identifications can be a burden to
formalization.

In the present work we reposition the concept of an identification not
as a reformulation of equality, which remains in its conventional
role, but as a manifestation of the higher-dimensional structure of
types formulated here as abstract cubes, following the suggestion of
Coquand and of Licata and Brunerie. The familiar elements of a type
are its points, identifications of points are lines, identifications
of lines are squares, and so forth through all finite
dimensions. Crucially, identifications have computational content,
both intrinsically as, for example, equivalences between types, and
extrinsically, as operationalized by constructive analogues of the Kan
condition familiar from mathematical homotopy theory. The resulting
type theory extends computational type theory to higher dimensions,
without losing the expressiveness of the original form.