Encoding type universes without using matching modulo AC, 14 pages, accepted at FSCD'22.

The encoding of proof systems and type theories in logical frame- works is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which var- ious systems have already been encoded, including type systems with an infinite hierarchy of universes with, on universes, a unary successor operator and a bi- nary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the proposed encodings use rewrit- ing with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to add in standard algorithms for β-reduction and type-checking. In this paper, we show that we can get rid of matching modulo AC by enforcing terms to be in some special canonical form wrt AC, and by using rewriting rules taking advantage of this canonical form.