Contents

Idea

In type theory, a type of (small) types – usually written $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

$\vdash A : Type$

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

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

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

In homotopy type theory the type of types $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 $Type : 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 $Type_0 : Type_1$ and $Type_1 : 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.

References

Detailed discussion of the type of types in Coq is in

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 $\mathcal{U}_n$ is not an $n$-type May 2013 (pdf)