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?
> 
> 
> 



How should I be thinking about object classifiers / universal fibrations / universes?
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.


