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\"of 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.

翻译：参数性是类型论语法的一个性质，例如它表明多态恒等函数类型中仅存在唯一函数。参数性通常通过外部方式证明，且不满足内部化条件。内部化之所以困难，是因为一旦存在见证参数性的项，该参数性本身也必须具有参数性，这将导致高维立方体的出现。在先前具有内部参数性的理论中，要么显式引入了高阶立方体的语法，要么通过区间这一新种类扩展原有理论。本文提出了一种具有内部参数性的类型论，它是对马丁-洛夫类型论的简单扩展：仅需增加若干新类型构造子、项构造子及等式。该语法中几何结构并非显式存在，而是涌现的：新运算与等式仅涉及维度不超过3的对象。我们证明该理论可由BCH立方体范畴上的预层建模，由于采用基于张成而非关系的参数性方法，无需纤维性条件。通过为该理论构造胶合模型，我们证明了外部参数性和正则性成立。该理论可视为新型模态类型论的特殊情形，也是展示高阶观测类型论计算性质的最简框架。