Document Open Access Logo

Type Theory with Explicit Universe Polymorphism

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2022.13.pdf
  • Filesize: 0.74 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • universes in type theory
  • universe polymorphism
  • level-indexed products
  • constraint-indexed products

Metrics

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

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.

Cite As Get BibTex

Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.TYPES.2022.13

Author Details

Marc Bezem
  • University of Bergen, Norway
Thierry Coquand
  • University of Gothenburg, Sweden
Peter Dybjer
  • Chalmers University of Technology, Gothenburg, Sweden
Martín Escardó
  • University of Birmingham, UK

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.

References

  1. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proceedings of the ACM on Programming Languages, 2(POPL):23:1-23:29, 2018. URL: https://doi.org/10.1145/3158111.
  2. Ali Assaf. A calculus of constructions with explicit subtyping. In 20th International Conference on Types for Proofs and Programs, TYPES, pages 27-46, 2014. Google Scholar
  3. Franz Baader and Jörg H. Siekmann. Unification theory. In Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2, Deduction Methodologies, pages 41-126. Oxford University Press, 1994. Google Scholar
  4. Marc Bezem and Thierry Coquand. Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. Theoretical Computer Science, 913:1-7, 2022. URL: https://doi.org/10.1016/j.tcs.2022.01.017.
  5. Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. The Burali-Forti argument in HoTT/UF with applications to the type of groups in a universe. https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.BuraliForti.html, 2022.
  6. Luca Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8(2):147-172, 1987. URL: https://doi.org/10.1016/0167-6423(87)90019-0.
  7. Mario Carneiro. The type theory of Lean. Master Thesis, Carnegie-Mellon University, 2019. Google Scholar
  8. Antoine Chambert-Loir. A presheaf that has no associated sheaf. https://freedommathdance.blogspot.com/2013/03/a-presheaf-that-has-no-associated-sheaf.html, 2013.
  9. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56-68, 1940. Google Scholar
  10. Thierry Coquand. Canonicity and normalization for dependent type theory. Theoretical Computer Science, 777:184-191, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.015.
  11. Judicaël Courant. Explicit universes for the calculus of constructions. In Theorem Proving in Higher Order Logics, TPHOLs, volume 2410 of Lecture Notes in Computer Science, pages 115-130. Springer, 2002. URL: https://doi.org/10.1007/3-540-45685-6_9.
  12. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Conference on Automated Deduction (CADE-25), volume 9195 of Lecture Notes in Computer Science, pages 378-388, 2015. Google Scholar
  13. Martín Hötzel Escardó. Introduction to univalent foundations of mathematics with Agda. CoRR, 2019. URL: https://arxiv.org/abs/1911.00580.
  14. Martín Hötzel Escardó et al. TypeTopology. https://www.cs.bham.ac.uk/~mhe/TypeTopology/index.html. Agda development.
  15. Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating proofs from an impredicative type system to a predicative one. In Computer Science Logic (CSL), 2023. Google Scholar
  16. Jean-Yves Girard. Thèse d'État. PhD thesis, Université Paris VII, 1971. Google Scholar
  17. Jean Giraud. Cohomologie non abélienne. Springer, 1971. URL: https://doi.org/10.1007/978-3-662-62103-5.
  18. Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89:107-136, 1991. Google Scholar
  19. Hugo Herbelin. Type inference with algebraic universes in the Calculus of Inductive Constructions. http://pauillac.inria.fr/~herbelin/articles/univalgcci.pdf, 2005.
  20. Gérard Huet. Extending the calculus of constructions with Type:Type. unpublished manuscript, April 1987. Google Scholar
  21. Per Martin-Löf. On the strength of intuitionistic reasoning. Preprint, Stockholm University, 1971. Google Scholar
  22. Per Martin-Löf. A theory of types. Preprint, Stockholm University, 1971. Google Scholar
  23. Per Martin-Löf. An intuitionistic theory of types. Preprint, Stockholm University, 1972. Google Scholar
  24. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium `73, pages 73-118. North Holland, 1975. Google Scholar
  25. Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153-175. North-Holland, 1982. Google Scholar
  26. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  27. Egbert Rijke, Elisabeth Bonnevier, Jonathan Prieto-Cubides, Fredrik Bakke, and others. Univalent mathematics in Agda. URL: https://github.com/UniMath/agda-unimath/.
  28. Carlos Simpson. Computer theorem proving in mathematics. Letters in Mathematical Physics, 69(1-3):287-315, July 2004. URL: https://doi.org/10.1007/s11005-004-0607-9.
  29. Matthieu Sozeau. Explicit universes. URL: https://coq.inria.fr/refman/addendum/universe-polymorphism.html#explicit-universes.
  30. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq. In Interactive Theorem Proving (ITP), 2014. Google Scholar
  31. Thomas Streicher. Semantics of Type Theory. Birkhäuser, 1991. Google Scholar
  32. Agda team. The Agda manual. URL: https://agda.readthedocs.io/en/v2.6.2.1/.
  33. The 1Lab Development Team. The 1Lab. URL: https://1lab.dev.
  34. The Agda Community. Agda standard library. URL: https://github.com/agda/agda-stdlib.
  35. The Coq Community. Coq. URL: https://coq.inria.fr.
  36. The Cubical Agda Community. A standard library for Cubical Agda. URL: https://github.com/agda/cubical.
  37. The HoTT-Agda Community. HoTT-Agda. URL: https://github.com/HoTT/HoTT-Agda.
  38. François Thiré. Interoperability between proof systems using the logical framework Dedukti. (Interopérabilité entre systèmes de preuve en utilisant le cadre logique Dedukti). PhD thesis, École normale supérieure Paris-Saclay, Cachan, France, 2020. URL: https://tel.archives-ouvertes.fr/tel-03224039.
  39. Vladimir Voevodsky. Universe polymorphic type system. http://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#UPTS, 2014.
  40. William C. Waterhouse. Basically bounded functors and flat sheaves. Pacific Math. J, 57(2):597-610, 1975. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact