Computational Higher Type Theory I: Abstract Cubical Realizability

Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-L"of's meaning explanations for constructive type theory define the concept of a type in terms of computation. Briefly, a type is a complete (closed) program that evaluates to a canonical type whose members are complete programs that evaluate to canonical elements of that type. The explanation is extended to incomplete (open) programs by functionality: types and elements must respect equality in their free variables. Equality is evidence-free---two types or elements are at most equal---and equal things are implicitly interchangeable in all contexts. Higher-dimensional type theory extends type theory to account for identifications of types and elements. An identification witnesses that two types or elements are explicitly interchangeable in all contexts by an explicit transport, or coercion, operation. There must be sufficiently many identifications, which is ensured by imposing a generalized form of the Kan condition from homotopy theory. Here we provide a Martin-L"of-style meaning explanation of simple higher-dimensional type theory based on a programming language that includes Kan-like constructs witnessing the computational meaning of the higher structure of types. The treatment includes an example of a higher inductive type (namely, the 1-dimensional sphere) and an example of Voevodsky's univalence principle, which identifies equivalent types. The main result is a computational canonicity theorem that validates the computational interpretation: a closed boolean expression must always evaluate to a boolean value, even in the presence of higher-dimensional structure. This provides the first fully computational formulation of higher-dimensional type theory.