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.

本文探讨了构造基础数学的概念以及基于马丁 - 勒夫的含义阐释的构造类型理论，通过电脑程序语言提供了一种可行的理论意义解释并解释了更高维的类型理论，并提供了完整的计算公式以证明该理论。