Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
According to the Wikipedia article on intuitionsitic type theory:
The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the universe type $U_0$ can be mapped to a type created with any combination of $0, 1, 2, \Sigma, \Pi, =$, and the inductive type constructor.
Would you please explain and elaborate further on how the universe types allow proofs to be written about other types?
In ordinary set theory one can write statements about all sets using the universal quantifier "$\forall x$" to have $x$ range over all sets.
In type theory without universes there is nothing that allows you to make a type that refers to all types. For example, the statement
"For all types $A$ and $B$, $A \times B$ and $B \times A$ are equivalent types."
is not a judgement in type theory. It is a meta-statement in which $A$ and $B$ are schematic symbols. In order to express it as a judgement in type theory, we need something else. One solution is to have a universe (and another to have polymorphism a la System $F$). With a universe $U$, we can use "$\prod_{A : U}$" to make a product type that ranges over "for all types $A$ (in the universe $U$)", inside type theory. For instance, the type $$\prod_{A : U} \prod_{B : U} (A \times B \simeq B \times A),$$ where $X \simeq Y$ is the type of equivalences from $X$ to $Y$, is how one would express the above statement using types.
type:type, otherwise they will be inconsistent (this was discovered by J.-Y. Girard in his Une extension de l'interpretation fonctionelle de Gödel a l'analyse). $\endgroup$