一句话：提出单值参数性并在 Coq 中实现透明传输框架，使定义与定理可在等价类型间像相等一样迁移。
同伦类型论通过单值性原理统一了类型论中的相等与等价，但现有证明助手多将其视为公理，难以在内部处理。本文提出单值参数性，通过强化参数性来保证类型等价在传输下保持，从而把单值性的好处带给程序员与证明者。作者在 Coq 中实现了一个轻量框架，使用户能像类型相等一样，透明地把定义和定理传输到等价类型；方法同时处理类型依赖与项依赖。文章还研究如何最大化这些传输的计算效果，并识别出一个可保证单值传输有效的片段。该工作为支持“模等价”的无缝编程与证明、构建更易用的认证编程环境铺平道路。
Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet clear how to extend them to handle univalence internally. In this paper, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. In particular, univalent parametricity strengthens parametricity to ensure preservation of type equivalences. We present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. Our approach handles both type and term dependency. We study how to maximize the effectiveness of these transports in terms of computational behavior, and identify a fragment useful for certified programming on which univalent transport is guaranteed to be effective. This work paves the way to easier-to-use environments for certified programming by supporting seamless programming and proving modulo equivalences.
@article{paperbot290,
title = {Equivalences for free: univalent parametricity for effective transport},
author = {Nicolas Tabareau and Éric Tanter and Matthieu Sozeau},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236787}
}