nLab type universe

Contents

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
completely presented setdiscrete object/0-truncated objecth-level 2-type/set/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
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 type theory, a type universe – usually written TypeType – is a type whose terms are either themselves types (type universes a la Russell), or representations of types in an internal model of the type theory (type universes a la Tarski). Either way, it is a universe of (small) types, a universe in type theory, and sometimes called a type of types.

One also speaks of TypeType as being a reflection of the type system in itself (e.g. MartinLöf 74, p. 6, Palmgren, pp. 2-3, Rathjen, p. 1, Luo 11, section 2.5, Luo 12, p. 2, Stanf. Enc. Phil.), following the reflection principle in set theory.

In homotopy type theory a type of (small) types is what in higher categorical semantics is interpreted as a (small) object classifier. Thus, the type of types is a refinement of the type of propositions which only contains the (-1)-truncated/h-level-1 types (and is semantically a subobject classifier).

In the presence of a type universe a judgement of the form

A:Type \vdash A : Type

says that AA is a term of type TypeType, hence is either a (small) type itself (for universes a la Russell), or a representation of types in an internal model of the type theory (for universes a la Tarski).

More generally, in universes a la Russell a hypothetical judgement of the form

x:XA(x):Type x : X \vdash A(x) : Type

says that AA is an XX-dependent type.

In universes a la Tarski the corresponding hypothetical judgment would be of the form

x:XEl(A)(x)type x : X \vdash El(A)(x)\; type

In homotopy type theory the type universe TypeType is often assumed to satisfy the univalence axiom. This is a reflection of the fact that in its categorical semantics as an object classifier is part of an internal (∞,1)-category in the ambient (∞,1)-topos: the one that as an indexed category is the small codomain fibration.

Per Martin-Lof‘s original type theory contained a type universe a la Russell which contained all types, which therefore in particular contained itself, i.e. one had Type:TypeType : Type. But it was pointed out by Jean-Yves Girard that this was inconsistent; see Girard's paradox. Thus, modern type theories generally contain a hierarchy of types universes, with

n:Type(n):Type(n+1)n:\mathbb{N} \vdash Type(n) : Type(n + 1)

for universes a la Russell, and

n:Type(n)typen:\mathbb{N} \vdash Type(n)\; type
n:Type (n):Type(n+1)n:\mathbb{N} \vdash Type^{'}(n) : Type(n + 1)
n:El n+1(Type (n))Type(n)n:\mathbb{N} \vdash El_{n+1}(Type^{'}(n)) \equiv Type(n)
n:El n,n+1:Type(n)Type(n+1)n:\mathbb{N} \vdash El_{n,n+1}:Type(n) \to Type(n + 1)
n:p:is1Monic(El n,n+1)n:\mathbb{N} \vdash p:is1Monic(El_{n,n+1})

for universes a la Tarski.

Formalizations

Type Universe à la Russell

A universe à la Russell is a type whose terms are types. In the presence of a separate judgmentAtypeA \;type”, this can be formulated as a deduction rule of the form

A:UAtype\frac{A:U}{A \;type}

Thus, the type formers have rules saying which universe they belong to, such as:

A:UB:AUΠAB:U\frac{A:U\quad B:A\to U}{\Pi\, A\, B : U}

With universes à la Russell, we can also omit the judgment “AtypeA\; type” and replace it everywhere by a judgment that A is a term of some universe. This is the approach taken by the HoTT textbook and by Coq.

Type Universe à la Tarski

A universe à la Tarski (Hofmann, section 2.1.6, Luo 12, Gallozzi 14, p. 40) is a type UU together with an “interpretation” operation allowing us to regard its terms as codes or names for actual types. Thus we have a rule such as

A:UEl(A)type\frac{A:U}{El(A)\;type}

saying that for each term AA of the type universe UU there is an actual type El(A)El(A). (Conversely, with notation as used at object classifier in an (infinity,1)-topos, one might write A=El(A)A = 'El(A)' to indicate that AA is the name of the type El(A)El(A) in the type universe.)

We usually also have operations on the universe corresponding to (but not identical to) type formers, such as

A:UB:AUπ(A,B):U\frac{A:U\quad B:A\to U}{\pi(A, B) : U}

with an equality El(π(A,B))=ΠEl(A)El(B)El(\pi(A,B))=\Pi \, El(A)\, El(B). Usually this latter equality (and those for other type formers) is a judgmental equality. If it is only an equivalence (i.e. we have a rule which gives us a canonical term of the equivalence type), we may speak of a weakly à la Tarski universe (Gallozzi 14, p. 49-50).

We can give a slightly different definition of weakly à la Tarski universe using propositional equality and a larger universe. More precisely, we can consider two (or many) universes UU and UU' with the usual rules for the relative reflection el(a):Uel(a):U' for any a:Ua:U, a choice of weakly or strongly a la Tarski computation rules for the reflections ElEl and ElEl', and a computation rule for the relative reflection el of UU inside UU' based on propositional equality, which gives us canonical elements of the identity types Id U(π(el(a),el(b)),el(π(a,b)))Id_{U'}(\pi'(el(a),el(b)),el(\pi(a,b))) and similarly for the other type formers.

If the containing universe is univalent the two definitions turn out to coincide.

Universes defined internally via induction-recursion are (strongly) à la Tarski. Weakly à la Tarski universes are easier to obtain in semantics (see below): they are somewhat more annoying to use, but probably suffice for most purposes.

Hierarchy of type universes

Let PP be a preorder. Then, a PP-indexed hierarchy of type universes a la Russell is a hypothetical judgment

a:P,b:P,abU(a):U(b)a:P, b:P, a \leq b \vdash U(a) : U(b)

and a PP-indexed hierarchy of type universes a la Tarski is

Ptypea:P,b:Pabtypea:P,b:Pp: x:ab y:abx=ya:PU(a)type\frac{P\; type \quad a:P, b:P \vdash a \leq b\; type \quad a:P, b:P \vdash p: \prod_{x:a \leq b} \prod_{y:a \leq b} x = y}{a:P \vdash U(a)\; type}
Ptypea:P,b:Pabtypea:P,b:Pp: x:ab y:abx=yU (a):U(b)\frac{P\; type \quad a:P, b:P \vdash a \leq b\; type \quad a:P, b:P \vdash p: \prod_{x:a \leq b} \prod_{y:a \leq b} x = y}{U^{'}(a) : U(b)}
Ptypea:P,b:Pabtypea:P,b:Pp: x:ab y:abx=yEl b(U (a))U(a)\frac{P\; type \quad a:P, b:P \vdash a \leq b\; type \quad a:P, b:P \vdash p: \prod_{x:a \leq b} \prod_{y:a \leq b} x = y}{El_{b}(U^{'}(a)) \equiv U(a)}
Ptypea:P,b:Pabtypea:P,b:Pp: x:ab y:abx=yEl a,b:U(a)U(b)\frac{P\; type \quad a:P, b:P \vdash a \leq b\; type \quad a:P, b:P \vdash p: \prod_{x:a \leq b} \prod_{y:a \leq b} x = y}{El_{a,b}:U(a) \to U(b)}
Ptypea:P,b:Pabtypea:P,b:Pp: x:ab y:abx=yp:is1Monic(El a,b)\frac{P\; type \quad a:P, b:P \vdash a \leq b\; type \quad a:P, b:P \vdash p: \prod_{x:a \leq b} \prod_{y:a \leq b} x = y}{p:is1Monic(El_{a,b})}

A type theory may have multiple type universes.

Properties

Universe enlargement

Both Coq and Agda support universe polymorphism to deal with the issue of universe enlargement. Moreover, Coq supports typical ambiguity.

Cumulativity

A tower of universes is cumulative if A:U iA:U_i implies A:U i+1A:U_{i+1} (rather than, say, Lift(A):U i+1Lift(A):U_{i+1}).

Cumulative Russell universes have some issues; see for instance Luo 12.

  • Coq uses Russell style 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 non-cumulative Russell style universes.

  • The HoTT Book (first edition) uses cumulative Russell style universes.

Categorical semantics

Univalent type universes à la Russell have been shown to be interpreted in type-theoretic model categories presenting the base (∞,1)-topos ∞Grpd

(Kapulkin-Lumsdaine-Voevodsky 12) and more generally presenting (∞,1)-toposes of (∞,1)-presheaves over elegant Reedy categories (Shulman 13).

Discussion for general (∞,1)-toposes (of (∞,1)-sheaves) that should have implementation weakly à la Tarski (Gallozzi 14, p. 49-50) is in (Gepner-Kock 12).

For more on this see the respective sections at relation between type theory and category theory.

References

Some of the text above is adapted from the entry universe at the homotopy type theory web.

Type universes in Martin-Löf type theory originate around

  • Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118. (web)

Basic discussion of the syntax of type universes is in

Definition of type universes weakly à la Tarski is in

Detailed discussion of the type of types in Coq is in

See also around slide 8 of the survey

  • Frade, Calculus of inductive constructions (2008/2009) (pdf)

A formal proof in homotopy type theory that the type of homotopy n-types is not itself a homotopy nn-type (it is an (n+1)(n+1)-type) is in

  • Nicolai Kraus, C. Sattler, The universe 𝒰 n\mathcal{U}_n is not an nn-type May 2013 (pdf)

(∞,1)-Categorical semantics for univalent type universes is discussed in

Relation to injective types:

See also

Last revised on June 16, 2022 at 08:22:01. See the history of this page for a list of all contributions to it.