A Canonical Form for Universe Levels in Impredicative Type Theory

Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory. In Stefano Guerrini, Barbara König 0001, editors, 34th EACSL Annual Conference on Computer Science Logic, CSL 2026, Paris, France, February 23-28, 2026. Volume 363 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. [doi]

Abstract

Abstract is missing.