Logical frameworks can be used to translate proofs from a proof system to another one. For this purpose, we should be able to encode the theory of the proof system in the logical framework. The Lambda Pi calculus modulo theory is one of these logical frameworks. Powerful theories such as pure type systems with an infinite hierarchy of universes have been encoded, leading to partial encodings of proof systems such as Coq, Matita or Agda. In order to fully represent systems such as Coq and Lean, we introduce a representation of an infinite universe hierarchy with an impredicative universe and universe variables where universe equivalence is equality, and implement it as a terminating and confluent rewrite system.

翻译：逻辑框架可用于将证明从一个证明系统转换到另一个证明系统。为此，我们需能在逻辑框架中编码证明系统的理论。带模理论的Lambda Pi演算便是此类逻辑框架之一。诸如具有无限宇宙层级的纯类型系统等强大理论已被编码，从而实现了Coq、Matita或Agda等证明系统的部分编码。为了完整表示Coq和Lean等系统，本文引入了一种包含非直谓宇宙及宇宙变量的无限宇宙层级表示，其中宇宙等价即为相等，并将其实现为一个终止且合流的重写系统。