Type Theory with Explicit Universe Polymorphism

Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó

doi:10.4230/LIPIcs.TYPES.2022.13

Type Theory with Explicit Universe Polymorphism

Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

35 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	28th International Conference on Types for Proofs and Programs, TYPES 2022
Editors	Delia Kesner, Pierre-Marie Pedrot
Publisher	Schloss Dagstuhl
Pages	13:1-13:16
ISBN (Electronic)	9783959772853
DOIs	https://doi.org/10.4230/LIPIcs.TYPES.2022.13
Publication status	Published - 27 Jul 2023
Event	28th International Conference on Types for Proofs and Programs, TYPES 2022 - Nantes, France Duration: 20 Jun 2022 → 25 Jun 2022

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	269
ISSN (Print)	1868-8969

Conference

Conference	28th International Conference on Types for Proofs and Programs, TYPES 2022
Country/Territory	France
City	Nantes
Period	20/06/22 → 25/06/22

Bibliographical note

Funding Information:
Acknowledgements The authors are grateful to the anonymous referees for useful feedback, and to Matthieu Sozeau for an update on the current state of universe polymorphism in Coq. We acknowledge the support of the Centre for Advanced Study (CAS) at the Norwegian Academy of Science and Letters in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19.

Publisher Copyright:
© Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó.

Keywords

constraint-indexed products
level-indexed products
type theory
universe polymorphism
universes in type theory

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.TYPES.2022.13Licence: Creative Commons: Attribution (CC BY)

BezemM2022TypeFinal published version, 758 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

Bezem, M., Coquand, T., Dybjer, P., & Escardó, M. (2023). Type Theory with Explicit Universe Polymorphism. In D. Kesner, & P.-M. Pedrot (Eds.), 28th International Conference on Types for Proofs and Programs, TYPES 2022 (pp. 13:1-13:16). Article 13 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 269). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.TYPES.2022.13

@inproceedings{84a86967085e4053bb1a143b06c9e004,

title = "Type Theory with Explicit Universe Polymorphism",

abstract = "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.",

keywords = "constraint-indexed products, level-indexed products, type theory, universe polymorphism, universes in type theory",

author = "Marc Bezem and Thierry Coquand and Peter Dybjer and Mart{\'i}n Escard{\'o}",

note = "Funding Information: Acknowledgements The authors are grateful to the anonymous referees for useful feedback, and to Matthieu Sozeau for an update on the current state of universe polymorphism in Coq. We acknowledge the support of the Centre for Advanced Study (CAS) at the Norwegian Academy of Science and Letters in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19. Publisher Copyright: {\textcopyright} Marc Bezem, Thierry Coquand, Peter Dybjer, and Mart{\'i}n Escard{\'o}.; 28th International Conference on Types for Proofs and Programs, TYPES 2022 ; Conference date: 20-06-2022 Through 25-06-2022",

year = "2023",

month = jul,

day = "27",

doi = "10.4230/LIPIcs.TYPES.2022.13",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl",

pages = "13:1--13:16",

editor = "Delia Kesner and Pierre-Marie Pedrot",

booktitle = "28th International Conference on Types for Proofs and Programs, TYPES 2022",

address = "Germany",

}

Bezem, M, Coquand, T, Dybjer, P & Escardó, M 2023, Type Theory with Explicit Universe Polymorphism. in D Kesner & P-M Pedrot (eds), 28th International Conference on Types for Proofs and Programs, TYPES 2022., 13, Leibniz International Proceedings in Informatics, LIPIcs, vol. 269, Schloss Dagstuhl, pp. 13:1-13:16, 28th International Conference on Types for Proofs and Programs, TYPES 2022, Nantes, France, 20/06/22. https://doi.org/10.4230/LIPIcs.TYPES.2022.13

Type Theory with Explicit Universe Polymorphism. / Bezem, Marc; Coquand, Thierry; Dybjer, Peter et al.
28th International Conference on Types for Proofs and Programs, TYPES 2022. ed. / Delia Kesner; Pierre-Marie Pedrot. Schloss Dagstuhl, 2023. p. 13:1-13:16 13 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 269).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Type Theory with Explicit Universe Polymorphism

AU - Bezem, Marc

AU - Coquand, Thierry

AU - Dybjer, Peter

AU - Escardó, Martín

N1 - Funding Information: Acknowledgements The authors are grateful to the anonymous referees for useful feedback, and to Matthieu Sozeau for an update on the current state of universe polymorphism in Coq. We acknowledge the support of the Centre for Advanced Study (CAS) at the Norwegian Academy of Science and Letters in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19. Publisher Copyright: © Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó.

PY - 2023/7/27

Y1 - 2023/7/27

N2 - 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.

AB - 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.

KW - constraint-indexed products

KW - level-indexed products

KW - type theory

KW - universe polymorphism

KW - universes in type theory

UR - http://www.scopus.com/inward/record.url?scp=85169292649&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.TYPES.2022.13

DO - 10.4230/LIPIcs.TYPES.2022.13

M3 - Conference contribution

AN - SCOPUS:85169292649

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 13:1-13:16

BT - 28th International Conference on Types for Proofs and Programs, TYPES 2022

A2 - Kesner, Delia

A2 - Pedrot, Pierre-Marie

PB - Schloss Dagstuhl

T2 - 28th International Conference on Types for Proofs and Programs, TYPES 2022

Y2 - 20 June 2022 through 25 June 2022

ER -

Type Theory with Explicit Universe Polymorphism

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this