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.

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