一句话：提出一种无需显式区间或高维立方语法的内部参数性类型论，并以预层与胶合模型证明外部参数性与 canonicity。
参数性是类型论的重要性质，但通常仅在外部成立；内部化时，见证项自身也须参数，导致高维立方体出现。已有理论需显式高维立方语法或新增区间 sort。本文提出 Martin-Löf 类型论的简单扩展，加入少量类型/项构造子和等式，不显式引入几何，仅涉及至多 3 维对象。作者以 BCH 立方范畴上的预层建模；采用 span-based 而非 relational 参数性，故无需 fibrancy。胶合模型进一步推出外部参数性与 canonicity。该理论可看作新模态类型论的特例，也是展示 higher observational type theory 计算性质的最简设定。
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-Löf type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated.
@article{paperbot2639,
title = {Internal Parametricity, without an Interval},
author = {Thorsten Altenkirch and Yorgo Chamoun and Ambrus Kaposi and Michael Shulman},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632920}
}