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, <em>displacement algebras,</em> 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.
Thu 19 JanDisplayed time zone: Eastern Time (US & Canada) change
15:10 - 16:25
|Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper
|An Order-Theoretic Analysis of Universe Polymorphism
Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of MinnesotaDOI
|Impredicative Observational Equality