Using Allen's method [5] one can define n universes of #Nuprl in n+1 predicative universes of Coq [1, sec. 6.1].
It is just too ugly because of duplications of definitions at each level.
I think we can formalize n universes of the predicative fragment of Coq in n+1 universes of Nuprl.
https://sympa.inria.fr/sympa/arc/coq-club/2014-08/msg00128.html