(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
basic constructions:
strong axioms
further
This page is about the concept in type theory. For the analogous concept in computer science see at polymorphism. For the concept introduced by Shinichi Mochizuki in inter-universal Teichmüller theory, see at poly-morphism.
In (homotopy) type theory, by universe polymorphism one refers to the ability for definitions to be implicitly duplicated at different type universe-levels, with the types they contain. Both Russell and Tarski style universes can be polymorphic or not.
Coq uses Russell style universes and used to have a sort of “fake” universe polymorphism, but recent versions of Coq have real universe polymorphism (thanks to Mathieu Sozeau).
Agda uses non-cumulative Russell style universes with universe polymorphism.
The HoTT Book (first edition) uses Russell style universes with universe polymorphism.
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.
Favonia, Carlo Angiuli, Reed Mullanix, An Order-Theoretic Analysis of Universe Polymorphism, Proceedings of the ACM on Programming Languages 7 57 (2023) 1659–1685 [doi:10.1145/3571250]
Last revised on December 15, 2023 at 17:22:31. See the history of this page for a list of all contributions to it.