Generalized Universe Hierarchies and First-Class Universe Levels

TL;DR

This paper develops a comprehensive framework for universe hierarchies in type theories, allowing for flexible, transfinite, and first-class universe levels with internal reasoning capabilities.

Contribution

It introduces a unified syntax and semantics for cumulative universe hierarchies, including transfinite levels and first-class universe levels with internal operations.

Findings

Semantics using induction-recursion for transfinite hierarchies

Lifting operations on type codes preserve type formers

Generalization of bounded polymorphism and internal level computations

Abstract

In type theories, universe hierarchies are commonly used to increase the expressive power of the theory while avoiding inconsistencies arising from size issues. There are numerous ways to specify universe hierarchies, and theories may differ in details of cumulativity, choice of universe levels, specification of type formers and eliminators, and available internal operations on levels. In the current work, we aim to provide a framework which covers a large part of the design space. First, we develop syntax and semantics for cumulative universe hierarchies, where levels may come from any set equipped with a transitive well-founded ordering. In the semantics, we show that induction-recursion can be used to model transfinite hierarchies, and also support lifting operations on type codes which strictly preserve type formers. Then, we consider a setup where universe levels are first-class types and subject to arbitrary internal reasoning. This generalizes the bounded polymorphism features of Coq and at the same time the internal level computations in Agda.