Type Theory with Explicit Universe Polymorphism (revised and extended version)

TL;DR

This paper refines and extends type theory with explicit universe polymorphism, incorporating universe levels, constraints, and indexed products, enhancing the expressiveness and precision of universe management.

Contribution

It introduces a system with explicit universe levels, constraints, and indexed products, advancing the formalization of universe polymorphism in type theory.

Findings

System includes judgments for internal universe levels.

Supports equality of universe levels.

Enables products indexed by universe levels and constraints.

Abstract

The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.