A Metatheoretic Analysis of Subtype Universes // Errata

Definition 4 — $\mathcal{L}_{\Gamma}$ is poorly defined. This is due to its treatment of dependent function types $\Pi (x : A) \cdot B$ and dependent pair types $\Sigma (x : A) \cdot B$. For any $\Gamma$ where $\Gamma, x : A \vdash B$, it’s possible for $B$ to inhabit a higher type universe than each $[a/x]B$, where $a : A$. As a result, $\mathcal{L}_{\Gamma}$ works for all simple types, but isn’t correct for dependent types. This is fixed in the full follow-up paper, which examines subtype universes in a type theory with type universes — the type theory in this work can be considered a subsystem of that type theory in that work.

Lemma 5 — The list item ’$\exists s$ such that $\Gamma \vdash A \stackrel{.}{=} {\sigma_{1}}(s)$’ should be ommitted from this list. It’s relatively simple to construct a set $\mathcal{C}$ such that there exists distinct $s, s'$ where $\Gamma \vdash {\sigma_{1}}(s) \stackrel{.}{=} {\sigma_{1}}(s')$. This does not affect any other proof content.

Theorem 8, Corollary 9 — Due to the use of coercive subtyping introducing a two-step reduction process, these are both incomplete statements and proofs. Any well-typed term with no holes will reduce to something of equal or lesser type level, but due to the presence of $\sigma_1, \sigma_2$ allowing for some amount of computation over types, it’s possible that a coercion may be inserted which is of a greater type level than the original object. Thankfully, the rest of the results do not depend on either of these statements, and so one could prove (after establishing the embedding) that for every type $M$ with normal form $N$, one has ${\mathcal{L}_{\Gamma}}(N) \leq {\mathcal{L}_{\Gamma}}(M)$.