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 a partial algorithm which uses a constraint-postponement strategy for trying 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中尚不可用。