Universe Management in UniMath
Master Project

Project Description

Universes in type theory are types whose elements are themselves types. To avoid logical inconsistencies, a universe cannot be an element of itself; otherwise, paradoxes such as Russell’s famous paradox (in set theory) and Girard’s paradox (a type-theoretic analog to Russell’s paradox) arise. Instead, proof assistants such as Coq, Agda, or Lean feature a hierarchy of universes, where “lower” universes are elements of “higher” universes.

The UniMath library of univalent mathematics, building on top of Coq, was initiated by Fields Medalist Vladimir Voevodsky as a testbed for his univalent foundations. UniMath currently deactivates universe management, as a hack, in order to implement Voevodsky’s resizing rules (see also slides from a talk by Voevodsky). Resizing rules allow one to assume that certain types are in a lower universe than what would be computed mechanically by the universe management of the underlying logic. Resizing rules should be justified by a suitable semantic model in which these rules can be proved to hold.

However, the deactivation of universe management for the purpose of implementing resizing is a very coarse hack, since it renders UniMath inconsistent: it is currently possible to construct a proof of False in UniMath.

An improvement would be to

• confine the deactivation of universe management in UniMath to specific (small, well-understood) files, into which the implementation of the resizing rules is quarantined; and
• reactivate universe management in the other files.

Project Goals

In this project, you will work on (some of) the following goals:

• Describe and compare universe management in the computer proof assistants Coq, Agda, and Lean
• Understand Voevodsky’s resizing rules and different ways to realize them in a computer proof assistant
• Implement a “file-by-file” usage of universe deactivation in UniMath
• Construct a model of resizing rules

Contacts for the Project

• Benedikt Ahrens (TU Delft)
• Kobe Wullaert (TU Delft)