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?

  • $\begingroup$ Universes are a stratification of types that prevents the well-known paradoxa of size! Just like in (ZF-like) set theories you cannot have a set of all sets, type-theories cannot have 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$ – Martin Berger Dec 14 '19 at 20:03
  • $\begingroup$ I knew about the paradoxes you mentioned and the role of hierarchy of type universes to prevent that, but still can not understand how universe types would allow proofs to be written about types? $\endgroup$ – al pal Dec 14 '19 at 20:11

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.

| cite | improve this answer | |
  • $\begingroup$ Thanks. Would you please also tell me how it would your example look if you had gone with the second solution which is to have polymorphism (System $F$)? $\endgroup$ – al pal Dec 14 '19 at 22:01
  • $\begingroup$ Hmm, I don't know about my example, but in System $F$ you can directly quantify over types, so you just write $\forall A$. How about if you Google "System F" and come back if you have specific questions? You're asking us to give you lectures on topics of interest. (Also note you're on the research-level site, and your question doesn't really fit.) $\endgroup$ – Andrej Bauer Dec 14 '19 at 22:32
  • $\begingroup$ You are right. Thanks for pointing it out. And thanks again for the answer. $\endgroup$ – al pal Dec 14 '19 at 23:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.