nLab hierarchy of universes

Redirected from "cumulativity".

Context

Universes

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

 Idea

In dependent type theory, having a type of all types results in various paradoxes, such as Russell's paradox and Girard's paradox. There are two ways to resolve this issue. One way is to simply add a universe of small types and accept that not all types are small. On the other hand, one can use a hierarchy of universes or universe hierarchy and postulate that every type is an element of universes in this universe hierarchy: Given an universe level κ\kappa, each type universe U κU_\kappa consists of only the U κU_\kappa-small types, and U κU_\kappa itself, while not an element of U κU_\kappa, is an element of the successor universe U κ +U_{\kappa^+}, where κ +\kappa^+ is the successor universe level. Most commonly used for the universe levels are the natural numbers, but other options are available as well, such as the integers or the ordinal numbers.

There are a few advantages of using a hierarchy of universes where every type is an element of the hierarchy, instead of a single separate type judgment, in the formulation of dependent type theory:

  1. Having a hierarchy of universes where every type in the type theory is an element of the hierarchy of universes avoids having to use long annotations everywhere. For example, if there is a single separate type judgment where not all types are elements of types, then given the type family x:AB(x)x:A \vdash B(x), if it is not small relative to the hierarchy of universes, then the heterogeneous identity type, elements a:Aa:A, b:Ab:A, p:Id A(a,b)p:\mathrm{Id}_A(a, b), y:B(a)y:B(a), and z:B(b)z:B(b) is represented by hId x:A.B(x)(a,b,p,y,z)\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z), where the subscript x:A.B(x)x:A.B(x) is a long annotation used to represent the type family x:AB(x)x:A \vdash B(x). With a hierarchy of universes where every type in the type theory is an element of the hierarchy of universes, the type family x:AB(x):Ux:A \vdash B(x):U is represented by the function B:AUB:A \to U, and the same heterogeneous identity type is then represented by hId B(a,b,p,y,z)\mathrm{hId}_{B}(a, b, p, y, z), which is more concise when written out, and in addition, the subscript BB is now represents that the type depends upon the universe, rather than merely being an annotation, and can be written as the dependent type hId(B,a,b,p,y,z)\mathrm{hId}(B, a, b, p, y, z).

  2. In the split context formalization of spatial type theory and cohesive type theory with an additional judgment for crisp terms of types, with a hierarchy of universes, one can define crisp types by simply postulating the type to crisply be an element of a type universe. However, without type universes, one has to add to the theory a separate judgment for crisp types, and all the requisite inference rules, structural rules, and congruence rules for crisp type judgments.

In addition, in dependent type theory with a hierarchy of universes,

However, with a single separate judgment for types, where not all types are elements of the hierarchy of universes, not all types can be compared using judgmental equality of terms, so neither of these are possible. There are two solutions to this, both of which are unwieldy:

However, this all comes at the cost of having to formalize the theory of universe levels of the hierarchy of universes before formalizing the type theory.

Definition

There are two main ways to define a hierarchy of universes:

  • The first way is done in dependent type theories with only a single separate type judgment, by defining a type of universe levels Level\mathrm{Level} inside the type theory and then defining a family of type universes indexed by Level\mathrm{Level}. Not all types are elements of universes in the universe hierarchy.

  • The second way is done in dependent type theories with either no separate type judgment à la Russell, or a separate type judgment for every type universe in the type theory à la Coquand, where every type in the theory is an element of the hierarchy of universes. Instead of having an internal type of universe levels, one has either a separate judgment κlevel\kappa \mathrm{level} which is in an untyped first-order theory or a meta-theoretic sort Level\mathrm{Level} which is in a typed first-order theory or a dependent type theory, with an operation which takes level κ\kappa to the successor level κ +\kappa^+. Then for type theories à la Russell one has for each level κ\kappa a universe U κ:U κ +U_\kappa:U_{\kappa^+}, and for type theories à la Coquand one has for each level κ\kappa a type judgment Atype κA \; \mathrm{type}_\kappa and a universe U κtype κ +U_\kappa \; \mathrm{type}_{\kappa^+}.

Cumulativity

Types of a universe U κU_\kappa in an hierarchy of universes are also types of the successor universe U κ +U_{\kappa^+}; i.e. U κU_\kappa is a subtype of U κ +U_{\kappa^+}. There are two different ways of representing this, reminiscent of the distinction between Russell universes and Tarski universes.

  • Given a universe level κ\kappa, the universe U κU_\kappa is cumulative if given an element A:U κA:U_\kappa, one can derive that A:U κ +A:U_{\kappa^+}. This is similar to Russell universes in that elements of a cumulative universe U κU_\kappa are literally elements of U κ +U_{\kappa^+}, similar to how elements of a Russell universe are literally types.

  • Given a universe level κ\kappa, the universe U κU_\kappa is non-cumulative if given a U κU_\kappa-small type A:U κA:U_\kappa, one can derive that Lift κ(A):U κ +\mathrm{Lift}_\kappa(A):U_{\kappa^+}. This is similar to Tarski universes in that elements of a cumulative universe U κU_\kappa are codes for elements of U κ +U_{\kappa^+}, represented by the family of elements A:U κLift κ(A):U κ +A:U_\kappa \vdash \mathrm{Lift}_\kappa(A):U_{\kappa^+}, similar to how elements of a Tarski universe are codes for types, represented by the family of types A:U κLift κ(A)typeA:U_\kappa \vdash \mathrm{Lift}_\kappa(A) \; \mathrm{type}.

Examples

Some examples of type theories with a hierarchy of universes are as follows:

  • Coq uses a hierarchy of Russell universes. For practical purposes, it also has cumulativity, although there is some question (perhaps mainly semantic) of whether this is true internally or whether it uses casts that are simply hidden from the user.

  • Agda uses a hierarchy of non-cumulative Russell universes.

  • UFP13 (first edition) uses a hierarchy of cumulative Russell universes.

  • Rijke 22 uses a hierarchy of non-cumulative Tarski universes.

References

The hierarchy of universes is discussed in section 1.3 of:

and in section 6.2 of:

Last revised on May 17, 2024 at 12:49:55. See the history of this page for a list of all contributions to it.