License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.28
URN: urn:nbn:de:0030-drops-157485
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15748/
Kovács, András
Generalized Universe Hierarchies and First-Class Universe Levels
Abstract
In type theories, universe hierarchies are commonly used to increase the expressive power of the theory while avoiding inconsistencies arising from size issues. There are numerous ways to specify universe hierarchies, and theories may differ in details of cumulativity, choice of universe levels, specification of type formers and eliminators, and available internal operations on levels. In the current work, we aim to provide a framework which covers a large part of the design space. First, we develop syntax and semantics for cumulative universe hierarchies, where levels may come from any set equipped with a transitive well-founded ordering. In the semantics, we show that induction-recursion can be used to model transfinite hierarchies, and also support lifting operations on type codes which strictly preserve type formers. Then, we consider a setup where universe levels are first-class types and subject to arbitrary internal reasoning. This generalizes the bounded polymorphism features of Coq and at the same time the internal level computations in Agda.
BibTeX - Entry
@InProceedings{kovacs:LIPIcs.CSL.2022.28,
author = {Kov\'{a}cs, Andr\'{a}s},
title = {{Generalized Universe Hierarchies and First-Class Universe Levels}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15748},
URN = {urn:nbn:de:0030-drops-157485},
doi = {10.4230/LIPIcs.CSL.2022.28},
annote = {Keywords: type theory, universes}
}
