Universe Management in UniMath
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.
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
Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: April 25, 2022