Type Theory with Explicit Universe Polymorphism (revised and extended version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2022
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914992440213504 |
|---|---|
| author | Bezem, Marc Coquand, Thierry Dybjer, Peter Escardó, Martín |
| author_facet | Bezem, Marc Coquand, Thierry Dybjer, Peter Escardó, Martín |
| contents | The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2212_03284 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Type Theory with Explicit Universe Polymorphism (revised and extended version) Bezem, Marc Coquand, Thierry Dybjer, Peter Escardó, Martín Logic in Computer Science 03B38 F.4.1 The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels. |
| title | Type Theory with Explicit Universe Polymorphism (revised and extended version) |
| topic | Logic in Computer Science 03B38 F.4.1 |
| url | https://arxiv.org/abs/2212.03284 |