Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have emerged with the aim of expressing such parametric reasoning in their internal logic, toward the end of solving various problems arising from the complexity of higher-dimensional coherence conditions in type theory. This paper presents a first step toward the unification, simplification, and extension of these various methods for internalizing parametricity. Specifically, I argue that there is an essentially modal aspect of parametricity, which is intimately connected with the category-theoretic concept of cohesion. On this basis, I describe a general categorical semantics for modal parametricity, develop a corresponding framework of axioms (with computational interpretations) in dependent type theory that can be used to internally represent and reason about such parametricity, and show this in practice by implementing these axioms in Agda and using them to verify parametricity theorems therein. I then demonstrate the utility of these axioms in managing the complexity of higher-dimensional coherence by deriving induction principles for higher inductive types, and in closing, I sketch the outlines of a more general synthetic theory of parametricity, with applications in domains ranging from homotopy type theory to the analysis of program modules.

翻译：参数性是类型系统的一种关键元理论性质，它意味着具备该性质的系统内部类型结构具有强一致性与模块化特性。近年来，出现了多种依赖类型理论系统，旨在通过其内部逻辑表达此类参数化推理，以解决类型理论中高维连贯条件复杂性所带来的各种问题。本文提出了统一、简化并扩展这些内化参数性多种方法的初步尝试。具体而言，本文论证了参数性本质上具有模态特性，这一特性与范畴论中的凝聚性概念紧密相关。在此基础上，我描述了一种模态参数性的通用范畴语义学，在依赖类型理论中建立了相应的公理框架（具备计算解释），可用于内部表示和推理此类参数性，并通过在Agda中实现这些公理并用以验证参数性定理来展示其实际应用。随后，我通过推导高阶归纳类型的归纳原理，证明了这些公理在管理高维连贯复杂性方面的实用性；最后，我勾勒出更广义的参数性综合理论框架，其应用领域涵盖从同伦类型理论到程序模块分析的广泛范畴。