Document Open Access Logo

Generalized Universe Hierarchies and First-Class Universe Levels

Author András Kovács

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.28.pdf
  • Filesize: 0.76 MB
  • 17 pages

Document Identifiers

Author Details

András Kovács
  • Eötvös Loránd University, Budapest, Hungary

Funding

The author was supported by the European Union, co-financed by the European Social Fund (EFOP-3.6.3-VEKOP-16-2017-00002).

Cite AsGet BibTex

András Kovács. Generalized Universe Hierarchies and First-Class Universe Levels. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.28

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • universes

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Peter Aczel. An introduction to inductive definitions. In Studies in Logic and the Foundations of Mathematics, volume 90, pages 739-782. Elsevier, 1977. Google Scholar
  2. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. ArXiv e-prints, May 2019. URL: http://arxiv.org/abs/1705.03307.
  3. Steve Awodey. Natural models of homotopy type theory. Math. Struct. Comput. Sci., 28(2):241-286, 2018. URL: https://doi.org/10.1017/S0960129516000268.
  4. Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, and Bas Spitters. Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci., 30(2):118-138, 2020. URL: https://doi.org/10.1017/S0960129519000197.
  5. Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. Relative induction principles for type theories. arXiv preprint, 2021. URL: http://arxiv.org/abs/2102.11649.
  6. John Cartmell. Generalised algebraic theories and contextual categories. PhD thesis, Oxford University, 1978. Google Scholar
  7. The Idris Community. Documentation for the idris language, 2021. URL: http://docs.idris-lang.org/en/latest/index.html.
  8. Thierry Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184-191, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.015.
  9. Agda developers. Agda documentation, 2021. URL: https://agda.readthedocs.io/en/v2.6.1.3/.
  10. Lean developers. Lean reference manual, version 3.3, 2021. URL: https://leanprover.github.io/reference/lean_reference.pdf.
  11. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer, 1995. URL: https://doi.org/10.1007/3-540-61780-9_66.
  12. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_11.
  13. Peter Dybjer and Anton Setzer. Indexed induction-recursion. J. Log. Algebraic Methods Program., 66(1):1-49, 2006. URL: https://doi.org/10.1016/j.jlap.2005.07.001.
  14. Neil Ghani, Lorenzo Malatesta, and Fredrik Nordvall Forsberg. Positive inductive-recursive definitions. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:13)2015.
  15. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proc. ACM Program. Lang., 3(POPL):3:1-3:28, 2019. URL: https://doi.org/10.1145/3290316.
  16. Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 492-506. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394736.
  17. Robert Harper and Robert Pollack. Type checking with universes. Theor. Comput. Sci., 89(1):107-136, 1991. URL: https://doi.org/10.1016/0304-3975(90)90108-T.
  18. Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for type theory. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 25:1-25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.25.
  19. Zhaohui Luo. Notes on universes in type theory. Lecture notes for a talk at Institute for Advanced Study, Princeton (URL: http://www. cs. rhul. ac. uk/home/zhaohui/universes. pdf), page 16, 2012. Google Scholar
  20. Per Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. Google Scholar
  21. Conor McBride. Datatypes of datatypes, 2015. URL: http://staff.mmcs.sfedu.ru/~ulysses/Edu/SSGEP/conor/conor.pdf.
  22. Erik Palmgren. On universes in type theory. In Twenty-five years of constructive type theory, volume 36 of Oxford Logic Guides, pages 191-204. Oxford University Press, 1998. Google Scholar
  23. Anton Setzer. Extending martin-löf type theory by one mahlo-universe. Arch. Math. Log., 39(3):155-181, 2000. URL: https://doi.org/10.1007/s001530050140.
  24. Jonathan Sterling. Algebraic type theory and universe hierarchies. CoRR, abs/1902.08848, 2019. URL: http://arxiv.org/abs/1902.08848.
  25. Jonathan Sterling and Carlo Angiuli. Normalization for cubical type theory. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  26. Amin Timany and Matthieu Sozeau. Cumulative inductive types in coq. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 29:1-29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.29.
  27. Taichi Uemura. A general framework for the semantics of type theory. CoRR, abs/1904.04097, 2019. URL: http://arxiv.org/abs/1904.04097.
  28. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  29. A. N. Whitehead and B. Russell. Principia mathematica. Revue de Métaphysique et de Morale, 19(2):19-19, 1911. Google Scholar
  30. Beta Ziliani and Matthieu Sozeau. A unification algorithm for coq featuring universe polymorphism and overloading. In Kathleen Fisher and John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 179-191. ACM, 2015. URL: https://doi.org/10.1145/2784731.2784751.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact