<p>In ordinary set theory one can write statements about <em>all</em> sets using the universal quantifier "<span class="math-container">$\forall x$</span>" to have <span class="math-container">$x$</span> range over all sets.</p>

<p>In type theory without universes there is nothing that allows you to make a type that refers to all types. For example, the statement</p>

<blockquote>
  <p>"For all types <span class="math-container">$A$</span> and <span class="math-container">$B$</span>, <span class="math-container">$A \times B$</span> and <span class="math-container">$B \times A$</span> are equivalent types."</p>
</blockquote>

<p>is not a judgement in type theory. It is a <em>meta-statement</em> in which <span class="math-container">$A$</span> and <span class="math-container">$B$</span> are <em>schematic</em> 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 <span class="math-container">$F$</span>). With a universe <span class="math-container">$U$</span>, we can use "<span class="math-container">$\prod_{A : U}$</span>" to make a product type that ranges over "for all types <span class="math-container">$A$</span> (in the universe <span class="math-container">$U$</span>)", inside type theory. For instance, the type
<span class="math-container">$$\prod_{A : U} \prod_{B : U} (A \times B \simeq B \times A),$$</span>
where <span class="math-container">$X \simeq Y$</span> is the type of equivalences from <span class="math-container">$X$</span> to <span class="math-container">$Y$</span>, is how one would express the above statement using types.</p>

CC BY-SA 4.0
2019-12-14T22:01:50.663Z
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$)?
al pal
CC BY-SA 4.0
2019-12-14T22:32:42.303Z
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.)
Andrej Bauer
CC BY-SA 4.0
2019-12-14T23:14:13.987Z
You are right. Thanks for pointing it out. And thanks again for the answer.
al pal
CC BY-SA 4.0
2019-12-14T20:59:51.010Z
2019-12-14T20:59:51.010Z
Andrej Bauer
<p>According to the <a href="https://en.wikipedia.org/wiki/Intuitionistic_type_theory" rel="nofollow noreferrer">Wikipedia article on intuitionsitic type theory</a>:</p>

<blockquote>
  <p>The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the universe type <span class="math-container">$U_0$</span> can be mapped to a type created with any combination of <span class="math-container">$0, 1, 2, \Sigma, \Pi, =$</span>, and the inductive type constructor.</p>
</blockquote>

<p>Would you please explain and elaborate further on how the universe types allow proofs to be written about other types?</p>

CC BY-SA 4.0
2019-12-14T20:03:06.113Z
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*).
Martin Berger
CC BY-SA 4.0
2019-12-14T20:11:40.163Z
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?
al pal
<type-theory>
What is the role of "universe" types in intuitionistic type theory?
al pal
# What is the role of "universe" types in intuitionistic type theory?

(Asked by: username_0 on 2019-12-14)

According to the [Wikipedia article on intuitionsitic type theory](https://en.wikipedia.org/wiki/Intuitionistic_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?

**Tags:** type-theory
> **Comments:**
> **username_1**: 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*).  
> **username_0**: 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?  

---

## 1 answers

### Answer by username_2 on 2019-12-14. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_0**: 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$)?  
> **username_2**: 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.)  
> **username_0**: You are right. Thanks for pointing it out. And thanks again for the answer.  

---

