一句话：用严格偏序范畴上的单子与位移代数刻画依赖类型论中的宇宙多态，并给出可实现的分层方案。
本文研究依赖类型论中轻量级宇宙多态（universe polymorphism）的语义与实现基础。作者提出用严格偏序范畴上的单子来刻画宇宙多态，并引入新的代数结构——位移代数（displacement algebra），在此基础上推广 McBride 的“粗略但有效分层”方案。文中给出若干奇异但一致的宇宙层级例子，并证明任意宇宙层级都可嵌入某个位移代数，从而可用该推广方案实现。多数技术结果在 Agda 中机器化验证，另提供基于位移代数的 OCaml 宇宙层级库，可供证明助手实现使用。
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.
@article{paperbot2055,
title = {An Order-Theoretic Analysis of Universe Polymorphism},
author = {Kuen-Bang Hou (Favonia) and Carlo Angiuli and Reed Mullanix},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571250}
}