(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
basic constructions:
strong axioms
further
For the concept in computer science see polymorphism. For the concept introduced by Shinichi Mochizuki in inter-universal Teichmüller theory, see poly-morphism.
Universe polymorphism is the ability for definitions to be implicitly duplicated at different universe levels, with the types they contain.
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.