Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems, when such obvious replacements are typically left implicit on paper. 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 Coq proof assistant, in the CoqElpi meta-language. We use this plugin on a gallery of representative examples of proof transfer issues in interactive theorem proving, and illustrate how Trocq covers the spectrum of several existing tools, used in program verification as well as in formalized mathematics in the broad sense.

翻译：形式化数学的库可能对同一数学概念使用广泛不同的表示。然而，当这些明显的替换在纸上通常被隐式地省略时，用户仍需付出或多或少的重大手动输入才能获得相应定理的变体。本文介绍Trocq，一种用于依赖类型理论的新证明传递框架。Trocq基于类型等价的新颖表述，用于推广单值参数性翻译。该框架尽可能避免依赖单值性公理，并且可用于比等价更广泛的关系。我们已在CoqElpi元语言中为Coq证明助手实现了相应的插件。我们在交互式定理证明中具有代表性的证明传递问题示例库上使用该插件，并展示Trocq如何覆盖多个现有工具的应用范围，这些工具既用于程序验证，也用于广义上的形式化数学。