一句话：提出 Trocq 证明转移框架，基于新的类型等价表述推广 univalent parametricity，并实现为 Coq 插件。
本文提出 Trocq，一个面向依赖类型论的新型证明转移框架。传统证明转移常受限于等价关系，并可能依赖 univalence 公理。Trocq 的核心是一种新的类型等价表述，它推广了 univalent parametricity 翻译，使得在可能时避免依赖 univalence 公理，并能处理比等价更一般的关系。作者将该框架实现为 Rocq/Coq 交互式定理证明器的插件，使用 Coq-Elpi 元语言编写。该工作为在依赖类型论中复用和迁移证明提供了更通用的机制，并展示了在证明助手中工程化实现该机制的可行性。
This article presents Trocq , a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Rocq/Coq interactive theorem prover, in the Coq-Elpi meta-language.
@article{CohenCM25,
title = {Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence},
author = {Cyril Cohen and Enzo Crance and Assia Mahboubi},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {3},
year = {2025},
doi = {10.1145/3737283}
}