Proof checking
Universe
A level used to organize types without placing every type inside itself.
Definition
Universe
A universe is a level in the type hierarchy used to classify types and avoid inconsistent self-reference.
A polymorphic declaration can refer to a universe variable rather than one fixed level. The kernel checks constraints among these levels.
01
Example
A generic identity function can work for a type α in any permitted universe.
02
Important distinction
Universe polymorphism does not mean one universe contains itself.
After reading this article, you should be able to
- Define Universe in the sense used on this site.
- Explain why type systems use a hierarchy of universes.