As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics to proof assistants based on predicative logics, whenever impredicativity is not used in an essential way. In this paper we present a transformation for sharing proofs with a core predicative system supporting prenex universe polymorphism (like in Agda). It consists in trying to elaborate each term into a predicative universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping each universe to a fixed one in the target theory is not sufficient in most cases. During the elaboration, we need to solve unification problems in the equational theory of universe levels. In order to do this, we give a complete characterization of when a single equation admits a most general unifier. This characterization is then employed in an algorithm which uses a constraint-postponement strategy to solve unification problems. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita's library to Agda, including proofs of Bertrand's Postulate and Fermat's Little Theorem, which (as far as we know) were not available in Agda yet.

翻译：形式化证明的编写是一项耗时的任务，因此设计共享已有证明的方法以避免重复工作至关重要。该领域的关键挑战之一在于，当非谓词性未被本质性使用时，如何将基于非谓词逻辑的证明助理中编写的证明迁移至基于谓词逻辑的证明助理。本文提出一种转换方法，通过支持预缀宇宙多态的核心谓词系统（如Agda）实现证明共享。该方法的核心思想是尽可能将每个项精化为最泛化的谓词宇宙多态项。宇宙多态的使用合理性在于：在目标理论中简单地将每个宇宙映射为固定宇宙在多数情况下是不充分的。精化过程中，我们需要在宇宙层次的等式理论中求解合一问题。为此，我们完整刻画了单等式存在最一般合一子的充要条件，并基于该刻画设计了采用约束延后策略的合一算法。所提出的转换方法虽为部分性方案，但在实践中可迁移许多未本质性使用非谓词性的证明。该方案已在Predicativize工具中实现，并成功将Matita库中多个非平凡数学内容（包括伯特兰假设和费马小定理的证明）半自动迁移至Agda——据我们所知，这些证明此前在Agda中尚不可用。