计算高级类型论I：抽象立体可实现性
Computational Higher Type Theory I: Abstract Cubical Realizability
摘要：
布劳威尔的数学建构主义基础是基于一个直观的有意义的概念计算共享的所有数学家。Martin-Löf对构造性类型论的意义解释定义了计算方面的类型概念。简单地说，一个类型是一个完整的（封闭的）程序，它计算为一个规范类型，其成员是计算为该类型的规范元素的完整程序。这个解释可以通过功能扩展到不完整的（开放的）程序：类型和元素必须尊重自由变量的相等性。平等是没有证据的-两种类型或元素最多是平等的-平等的东西在所有的上下文中都是隐含的可互换的。更高维的类型论扩展了类型论以解释类型和元素的标识。同一性证明了两种类型或元素在所有的上下文中都可以通过一种明确的传输或强制操作而明确地互换。必须有足够多的标识，这是通过从同伦理论中强加一个广义形式的Kan条件来保证的。在这里，我们提供了一个简单的高维类型论基于一个程序设计语言，其中包括类似Kan-like结构见证了类型的更高结构的计算意义的马丁-勒夫风格的意义解释。处理包括一个更高的归纳类型的例子（即1维球体）和Voevodsky的一价原则的例子，它确定了等价类型。主要结果是一个计算规范性定理，验证了计算解释：一个封闭的布尔表达式必须总是评估为布尔值，即使在存在更高维的结构。这提供了高维类型论的第一个完全计算公式。
英文摘要：
Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf'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öf-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
