免费的扩展类型
Extension Types for Free
浏览论文内容
中文总结 AI 辅助
本文将多种场景下的扩展类型统一到双层类型论框架，证明其对HoTT保守，验证了Riehl等的演算，还结合Agda形式化结果，为解决立方类型论对书式HoTT的保守性猜想提供了方法。
中文摘要 AI 辅助
扩展类型是依赖类型论中出现在多种场景的概念，其术语由部分条件确定，例如通过严格边界条件确定。典型例子包括立方类型论的路径类型（端点固定的路径）、Riehl与Shulman提出的命名扩展类型（子形状上固定的项），以及cooltt和Agda的受控展开机制（满足条件时固定的项）。每种类型论都配备了管理其规则的（元理论）面演算或形状层，并带有预期语义。我们将所有这些情况统一到一个无需新公理或模型构造的单一框架——双层类型论（two-level type theory, 2LTT）中，这一步在语义上是免费的：同伦类型论（HoTT）的标准模型自动成为2LTT的模型，且该理论对HoTT是保守的。扩展类型是可定义的，其定义验证了Riehl与Shulman的整个扩展类型演算：规则严格成立，假定的公理（如相对函数外延性）成为定理。由此，基础理论（HoTT）的每个模型都可生成带扩展类型的同理论模型，唯一真正的假设是哪些映射算作余纤维化。保守性使该框架成为比较类型论的工具。我们证明，适当形式下的立方胶合等价于万有性，在此基础上，我们提出一种方法以解决“立方类型论对书式HoTT是保守的”这一同伦类型论核心开放问题之一。本文主体的所有结果均在Agda--two-level中自动形式化，该开发结合了HoTT内部论证与HoTT外部推理。
英文摘要
Extension types are a concept in dependent type theory that has appeared in various contexts. The idea is to have types whose terms are partially determined, e.g. via a strict boundary condition. Standard examples are path types of cubical type theories (paths with fixed endpoints), Riehl and Shulman's name-giving extension types (terms fixed on subshapes), as well as the controlled-unfolding mechanism of cooltt and Agda (terms that are fixed if a condition is met). In each case, the type theory is equipped with a (meta-theoretic) face calculus, or shape layer, that governs their rules, and comes with intended semantics. We unify all these occurrences in a single framework where no new axioms or model constructions are needed, namely two-level type theory. This step, too, is free (semantically): the standard models of HoTT are automatically models of 2LTT, and the theory is conservative over HoTT. Extension types are definable, and the definition validates Riehl and Shulman's entire extension-type calculus: the rules hold strictly, and the postulated axioms, such as relative function extensionality, become theorems. In this way, every model of the base theory (HoTT) gives rise to a model of the same theory with extension types; the only genuine assumptions are which maps count as cofibrations. Conservativity makes the framework a tool for comparing type theories. We prove that cubical gluing, in a suitable formulation, is equivalent to univalence. On this basis, we suggest an approach toward the conjecture that cubical type theories are conservative over book HoTT, one of the central open problems of homotopy type theory. All results of the main body of the paper are auto-formalized in Agda --two-level, in a development that combines HoTT-internal arguments with reasoning that is external to HoTT.
