nLab universe polymorphism

Contents

Context

Universes

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

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.

Contents

Idea

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.

Examples and applications

  • 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.

References

Last revised on December 15, 2023 at 17:22:31. See the history of this page for a list of all contributions to it.