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.