  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, such as Coq, Matita
and the HOL family, to proof assistants based on predicative logics like Agda,
whenever impredicativity is not used in an essential way. In this paper we
present an algorithm to do such a translation between a core impredicative type
system and a core predicative one allowing prenex universe polymorphism like in
Agda. It consists in trying to turn a potentially impredicative term into a
universe polymorphic term as general as possible. The use of universe
polymorphism is justified by the fact that mapping an impredicative universe to
a fixed predicative one is not sufficient in most cases. During the algorithm,
we need to solve unification problems modulo the max-successor algebra on
universe levels. But, in this algebra, there are solvable problems having no
most general solution. We however provide an incomplete algorithm whose
solutions, when it succeeds, are most general ones. 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 arithmetic library to Agda, including
Bertrand's Postulate and Fermat's Little Theorem, which were not available in
Agda yet.
