Univalence 与参数性的结合

对所有人（包括数学家）而言，模等价进行推理都是自然的。遗憾的是，在基于类型论的证明助手中，等式令人头疼地是句法的，因此利用等价至多十分繁琐。参数性（parametricity）与 univalence 是已被探索用于跨类型等价传输程序与证明的两个主要概念，但它们都未能实现无缝、自动的传输。本文首先阐明了这两个概念各自孤立时的局限，随后设计了二者富有成效的结合。由此产生的概念——univalent parametricity（univalent 参数性）——是参数性的一种异质扩展，经 univalence 强化，可完整实现模等价的编程与证明。除 univalent 参数性的理论外，我们提出了一个在 Coq 中实现的轻量级框架，允许用户透明地将一个类型的定义与定理转移到等价类型上，如同它们相等一般。例如，只要证明两种表示等价，就能方便地在易于推理的表示与计算高效的表示之间切换。参数性与 univalence 的结合支持按需传输（transport à la carte）：源于类型等价的基 univalent 传输，可辅以这些类型上函数间等价性的额外证明，从而能够提升更多程序与证明，并生成更高效的项。我们在若干示例上展示了 univalent 参数性的使用，包括 Coq 中近期对原生整数的集成。