How should I be thinking about object classifiers / universal fibrations / universes?

Question

I have been learning about homotopy type theory this summer. I am not a homotopy theorist but I am more comfortable with homotopy theory than I am with type theory, so the way I rationalize many of the constructions used is by thinking in terms of homotopy theory. For example, when someone says type, i think homotopy type of a space. When someone says type family, I think of the family of fibers of some fibration. $ \Sigma $ types are total spaces and dependent function types are sections of a fibration. Things like path induction and function extensionality are easy to understand from this perspective.

One thing that I have never really understood is how to think about the universe $ \mathcal{U} $. It is a type, so it should be the homotopy type of some space? Assuming this, the univalence axiom says that there is one path component for every homotopy type. Moreover, we have some sort of universal fibration $$ \Sigma_{A : \mathcal{U}} A \to \mathcal{U} $$ and the fiber over the path component corresponding to the homotopy type $A$ has homotopy type $A$. I have read things like "Morally, $\mathcal{U}$ is an object classifier" and "$\Sigma_{A : \mathcal{U}} A \to \mathcal{U} $ behaves like a universal fibration", but i dont really know how to make intuitive sense of these statements.

Questions: How should I be thinking about the universe $ \mathcal{U}$? Is it the homotopy type of some huge space (ignoring set theoretic problems?) What does it mean to say $ \mathcal{U}$ behaves like an object classifier? What does it mean to say $\Sigma_{A : \mathcal{U}} A \to \mathcal{U}$ is a universal fibration?

Answer 1

Yes, the universe is the classifying space for small homotopy types. For various reasons, the universe is not itself a small homotopy type; so it fails to be an object classifier for the trivial reason that it does not classify itself.

Under the univalence axiom, the homotopy type of the universe is well-defined: it is the disjoint union of the classifying spaces $B \mathrm{Aut} (X)$. Note that there is a fibration over $B \mathrm{Aut} (X)$ whose fibres are $X$, such that every fibration with fibres $X$ occurs as a pullback of this fibration in a unique (up to homotopy) way. (This is the Borel construction $E \mathrm{Aut} (X) \times_{\mathrm{Aut} (X)} X$!) The universal fibration is just the disjoint union of these individual fibrations.

Answer 2

Zhen Lin's answer is great. Here is something I realized this morning (I believe this was one of the original motivations for the univalence axiom). You can make sense of the statement "$\Sigma_{(A : \mathcal{U})} A \to \mathcal{U}$ is a universal fibration" inside HoTT. Let us call a type family $P : B \to \mathcal{U}$ "fibration data". The corresponding fibration is $\Sigma_{(b : B)} P(b) \to B$. In the paper homotopy limits in type theory, homotopy pullbacks are constructed inside HoTT. Indeed, $$\require{AMScd} \begin{CD} \Sigma_{(a:A)} \Sigma_{\left( x:\Sigma_{(b:B)}P(b)\right)} (\pi_1(x) = f(a)) @>>> \Sigma_{(b:B)} P(b)\\ @VVV @VVV \\ A @>{f}>> B \end{CD}$$ is a homotopy pullback square. Note that, using the induction principle for $\Sigma$-types, it is easy to construct the homotopy that makes this square homotopy commutative. We have another homotopy commutative square $$\require{AMScd} \begin{CD} \Sigma_{(a:A)} P(f(a))@>>> \Sigma_{(b:B)} P(b)\\ @VVV @VVV \\ A @>{f}>> B \end{CD}$$ where the top map and the homotopy are constructed using $\Sigma$-induction. The universal property of homotopy pullbacks gives us a map $$ \Sigma_{(a : A)} P(f(a)) \to \Sigma_{(a : A)} \Sigma_{\left(x : \Sigma_{(b : B)}P(b)\right)} (\pi_1(x) = f(a)) $$ and homotopies making the obvious diagram commute up to homotopy. In fact, it is easy to construct the map and homotopies directly using $ \Sigma$-induction. Again, using $\Sigma$-induction and the introduction rule for equality types in a $\Sigma$-type we can construct a quasi-inverse to this map, so it is an equivalence. Moreover, this quasi-inverse fits into the appropriate homotopy commutative diagram, which tells us that the second commutative square above is in fact a homotopy pullback square. I worked all of this out explicitly this morning. It is a good exercise in working inside HoTT, so I won't spoil it for anyone else interested.

What all of this tells us is that given fibration data $P : A \to \mathcal{U}$, the corresponding fibration is the homotopy pullback of $\Sigma_{(A : \mathcal{U})} A \to \mathcal{U}$ along $P$.