A Canonical Form for Universe Levels in Impredicative Type Theory.

Yoan Gran

Browse the full CSL paper archive.