An Order-Theoretic Analysis of Universe Polymorphism

Kuen Bang Hou, Carlo Angiuli, Reed Mullanix

Research output: Contribution to journalArticlepeer-review


We present a novel formulation of universe polymorphism in dependent type theory in terms of monads on the category of strict partial orders, and a novel algebraic structure, displacement algebras, on top of which one can implement a generalized form of McBride's "crude but effective stratification"scheme for lightweight universe polymorphism. We give some examples of exotic but consistent universe hierarchies, and prove that every universe hierarchy in our sense can be embedded in a displacement algebra and hence implemented via our generalization of McBride's scheme. Many of our technical results are mechanized in Agda, and we have an OCaml library for universe levels based on displacement algebras, for use in proof assistant implementations.

Original languageEnglish (US)
Pages (from-to)1659-1685
Number of pages27
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
StatePublished - Jan 9 2023

Bibliographical note

Publisher Copyright:
© 2023 Owner/Author.


  • type theory
  • universe polymorphism
  • universes


Dive into the research topics of 'An Order-Theoretic Analysis of Universe Polymorphism'. Together they form a unique fingerprint.

Cite this