An Order-Theoretic Analysis of Universe Polymorphism
summary
Claims that universe polymorphism equals monads on strict partial orders and that every usable universe hierarchy embeds into newly defined displacement algebras, so McBride’s stratification generalizes to a universal implementation. Gives concrete exotic examples (integer and rational-indexed hierarchies), mechanizes many proofs in Agda, and supplies an OCaml library for universe levels. Proves embedding theorem and shows the generalized McBride construction actually implements those hierarchies.
AI-written summary · about
chapters (5)
- 0:00Start
- 10:41L-type theory well-typed terms e
- 12:09Universe Polymorphism Levels with variables
- 14:40The McBride Monad
- 15:42The Generalized McBride Monad
related talks
30mNormalisation for First-Class Universe Levels
16mEnhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…)
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
26mObservational Equality: Now for Good
21mPolymorphic Type Inference for Dynamic Languages
49mSemantic Foundations for Probabilistic Programming
14mThe Simple Essence of Monomorphization
23mFormalizing Monoidal Categories and Actions for Syntax with Binders