2026-09-15T15:40:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25464 2026-09-05T19:17:24Z ddc:004 open_access

A Canonical Form for Universe Levels in Impredicative Type Theory Géran, Yoan universe levels canonical form impredicativity imax algebra The 0-imax-successor algebra, where imax: ℕ × ℕ → ℕ is the function defined by imax(n, 0) = 0 and imax(n, S(m)) = max(n, S(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Rocq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yoan Géran 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.39 urn:nbn:de:0030-drops-254640 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.39 eng https://creativecommons.org/licenses/by/4.0/legalcode