Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bounded First-Class Universe Levels in Dependent Type Theory

Jonathan Chan, Stephanie Weirich

TL;DR

This work designs TTBFL, a minimal dependent type theory with bounded, first-class universe levels, parameterized over well-founded level sets and expressed in a syntax that treats levels as terms. It establishes key metatheoretic properties—subject reduction, type safety, consistency, and canonicity—via a formal mechanization in Lean and a syntactic logical relation that ties types to semantic interpretations across levels. Reduction is handled through parallel reduction and a robust conversion relation, enabling preservation and progress proofs, while normalization remains an open problem. The authors also outline extensions (level operators and subtyping) and discuss the implications for normalization and decidability, positioning TTBFL as a conservative, well-behaved foundation for higher-level universe calculations in proof assistants.

Abstract

In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from introducing logical inconsistency in the presence of type-in-type. The simplest mechanism is a hierarchy of universes indexed by a sequence of levels, typically the naturals. To improve reusability of definitions, they can be made level polymorphic, abstracting over level variables and adding a notion of level expressions. For even more expressive power, level expressions can be made first-class as terms themselves, and level polymorphism is subsumed by dependent functions quantifying over levels. Furthermore, bounded level polymorphism provides more expressivity by being able to explicitly state constraints on level variables. While semantics for first-class levels with constraints are known, syntax and typing rules have not been explicitly written down. Yet pinning down a well-behaved syntax is not trivial; there exist prior type theories with bounded level polymorphism that fail to satisfy subject reduction. In this work, we design an explicit syntax for a type theory with bounded first-class levels, parametrized over arbitrary well-founded sets of levels. We prove the metatheoretic properties of subject reduction, type safety, consistency, and canonicity, entirely mechanized from syntax to semantics in Lean.

Bounded First-Class Universe Levels in Dependent Type Theory

TL;DR

This work designs TTBFL, a minimal dependent type theory with bounded, first-class universe levels, parameterized over well-founded level sets and expressed in a syntax that treats levels as terms. It establishes key metatheoretic properties—subject reduction, type safety, consistency, and canonicity—via a formal mechanization in Lean and a syntactic logical relation that ties types to semantic interpretations across levels. Reduction is handled through parallel reduction and a robust conversion relation, enabling preservation and progress proofs, while normalization remains an open problem. The authors also outline extensions (level operators and subtyping) and discuss the implications for normalization and decidability, positioning TTBFL as a conservative, well-behaved foundation for higher-level universe calculations in proof assistants.

Abstract

In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from introducing logical inconsistency in the presence of type-in-type. The simplest mechanism is a hierarchy of universes indexed by a sequence of levels, typically the naturals. To improve reusability of definitions, they can be made level polymorphic, abstracting over level variables and adding a notion of level expressions. For even more expressive power, level expressions can be made first-class as terms themselves, and level polymorphism is subsumed by dependent functions quantifying over levels. Furthermore, bounded level polymorphism provides more expressivity by being able to explicitly state constraints on level variables. While semantics for first-class levels with constraints are known, syntax and typing rules have not been explicitly written down. Yet pinning down a well-behaved syntax is not trivial; there exist prior type theories with bounded level polymorphism that fail to satisfy subject reduction. In this work, we design an explicit syntax for a type theory with bounded first-class levels, parametrized over arbitrary well-founded sets of levels. We prove the metatheoretic properties of subject reduction, type safety, consistency, and canonicity, entirely mechanized from syntax to semantics in Lean.

Paper Structure

This paper contains 14 sections, 29 theorems, 13 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Motivation
  3. A minimal type theory with bounded first-class universe levels
  4. Type safety
  5. Reduction and conversion
  6. Subject reduction and type safety
  7. Consistency and canonicity
  8. Logical relation for closed types
  9. Fundamental soundness theorem
  10. Towards normalization
  11. Extensions
  12. Level operators and eliminators
  13. Subtyping
  14. Conclusion and future work

Key Result

Lemma 2

$\langle$\repo/tree/main/src/reduction.lean:parsSubst$\rangle$ If $\mathit{a} \Rightarrow^\ast \mathit{a'}$ and $\mathit{b} \Rightarrow^\ast \mathit{b'}$, then $\mathit{b} [ \mathit{x} \mapsto \mathit{a} ] \Rightarrow^\ast \mathit{b'} [ \mathit{x} \mapsto \mathit{a'} ]$.

Figures (7)

  • Figure 1: Syntax $\langle$\repo/tree/main/src/syntactics.lean:Term,Ctxt$\rangle$
  • Figure 2: Typing and selected equality rules (no universes or levels) $\langle$\repo/tree/main/src/typing.lean:Wtf,Eqv$\rangle$
  • Figure 3: Typing rules (universes and levels)
  • Figure 4: Parallel reduction rules $\langle$\repo/tree/main/src/reduction.lean:Par,Pars$\rangle$
  • Figure 5: Logical relation for closed types $\langle$\repo/tree/main/src/semantics.lean:Interps$\rangle$
  • ...and 2 more figures

Theorems & Definitions (32)

  • Definition 1: Conversion
  • Lemma 2: Substitution (p.r.)
  • Lemma 3: Construction (p.r.)
  • Lemma 4: Inversion (p.r.)
  • Lemma 5: Completion (p.r.)
  • Corollary 6: Diamond (p.r.)
  • Theorem 7: Confluence (p.r.)
  • Corollary 8: Properties of conversion
  • Lemma 9: Syntactic consistency
  • Lemma 10: Injectivity (conv.)
  • ...and 22 more