This is a formalization of the displacement algebras, their properties, and part of meta-theoretic analysis found in our POPL 2023 paper “An Order-Theoretic Analysis of Universe Polymorphism”. The accompanying OCaml implementation is at https://github.com/RedPRL/mugen/.
🚧 This repository is under major rewrites and cleanups. See version 0.1.0 for the code that matches the POPL 2023 paper.
🚧 The links are currently broken.
| Displacements | Paper Section | Agda Module | OCaml Module(s) |
|---|---|---|---|
| Natural numbers | 3.3.1 | Nat | Nat and Nat |
| Integers | 3.3.1 | Int | Int and Int |
| Non-positive integers | 3.3.1 | NonPositive | NonPositive and NonPositive |
| Constant displacements | 3.3.2 | Constant | Constant |
| Binary products | 3.3.3 | Product | Product and Product |
| Lexicographic binary products | 3.3.4 | Lexicographic | Lexicographic and Lexicographic |
| Indexed products | 3.3.5 | IndexedProduct | (not implementable) |
| Nearly constant infinite products | 3.3.5 | NearlyConstant | NearlyConstant and NearlyConstant |
| Infinite products with finite support | 3.3.5 | FiniteSupport | FiniteSupport and FiniteSupport |
| Prefix order | 3.3.6 | Prefix | Prefix |
| Fractal displacements | 3.3.7 | Fractal | Fractal |
| Opposite displacements | 3.3.8 | Opposite | Opposite |
| Weird fractal displacements | 3.3.9 (JFP only) | WeirdFractal | Fractal |
| Endomorphisms | 3.4 (Lemma 3.7) | Endomorphism | (not implementable) |
| Theorems | Paper Section | Agda Module |
|---|---|---|
| Traditional level polymorphism | 2.2 | Traditional |
| Validity of McBride monads | 3.1 | McBride |
| Embedding of endomorphisms | 3.4 (Lemma 3.8) | EndomorphismEmbedding |
| Embedding of small hierarchy theories | 3.4 (Lemma 3.9) | SubcategoryEmbedding |
| Universality of McBride monads | 3.4 (Theorem 3.10) | Universality |
Run the following command to check formalization.
docker build -t agda-mugen:edge .
docker run agda-mugen:edge