nLab
universe polymorphism

Contents

Context

Universes

Foundations

For the concept in computer science see polymorphism. For the concept introduced by Shinichi Mochizuki in inter-universal Teichmüller theory, see poly-morphism.

Contents

Idea

Universe polymorphism is the ability for definitions to be implicitly duplicated at different universe levels, with the types they contain.

Examples and applications

References

  • Robert Harper, Rober Pollack, Type Checking with Universes (1991) (web)

  • Mike Shulman, Universe Polymorphism and Typical Ambiguity, blog post 2012

  • Matthieu Sozeau and Nicolas Tabareau, Universe polymorphism in Coq, In: Klein G., Gamboa R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. doi

  • András Kovács, Generalized Universe Hierarchies and First-Class Universe Levels, 2021, arxiv:2103.00223.

Last revised on April 12, 2021 at 18:07:44. See the history of this page for a list of all contributions to it.