nLab
type of types

Idea

In type theory, a type of (small) types – usually written $\mathrm{Type}$ – is a type whose terms are themselves types. Thus, it is a universe of (small) types.

In homotopy type theory a type of (small) types is what semantically becomes 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 of types a judgement of the form

$$⊢A:\mathrm{Type}$$\vdash A : Type

says that $A$ is a term of type $\mathrm{Type}$, hence is a (small) type itself. More generally, a hypothetical judgement of the form

$$x:X⊢A(x):\mathrm{Type}$$x : X \vdash A(x) : Type

says that $A$ is an $X$-dependent type.

In homotopy type theory the type of types $\mathrm{Type}$ 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 (infinity,1)-category in the ambient (infinity,1)-topos: the one that as an indexed category is the small codomain fibration.

Per Martin-Lof’s original type theory contained a type of all types, which therefore in particular contained itself, i.e. one had $\mathrm{Type}:\mathrm{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 of types, with ${\mathrm{Type}}_0:{\mathrm{Type}}_1$ and ${\mathrm{Type}}_1:{\mathrm{Type}}_2$, etc.

Properties

Universe enlargement

Both Coq and Agda have systems to manage universe sizes and universe enlargement automatically; Agda’s is more advanced (universe polymorphism), whereas Coq’s is good enough for many purposes but tends to produce “universe inconsistencies” when working with univalence.

Related concepts

• universe polymorphism

• univalence

• Prop, the type of propositions,

  • subobject classifier

• object classifier

• parametric polymorphism

• Girard's paradox

References

• Erik Palmgren, On Universes in Type Theory (pdf)

Detailed discussion of the type of types in Coq is in

• Adam Chlipala, Certified programming with dependent types – Library Universes

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 $n$-type (it is an $(n+1)$-type) is in

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