9
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ You don't mean the identity to be universal, but rather the thing you call "some sort of universal fibration" in the displayed formula. $\endgroup$ – Andrej Bauer Jul 16 '14 at 16:06
  • $\begingroup$ good point! I edited the question. $\endgroup$ – Daniel Barter Jul 16 '14 at 16:11
10
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ Normally, the phrase object classifier is used with the understanding that only a large object can classify small objects. So the universe really is an object classifier. $\endgroup$ – Mike Shulman Jul 16 '14 at 23:02
  • 1
    $\begingroup$ Can we cook up a universe (in some non-trivial category) which classifies everything, including itself? Presumably a model of $\mathtt{Type} : \mathtt{Type}$ will do it, so various domain-theoretic models. $\endgroup$ – Andrej Bauer Jul 18 '14 at 17:56
3
$\begingroup$

Zhen Lin's answer is great. Here is somthing I realized this morning (I belive this was one of the origonal 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. Lets 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_{x:\Sigma_{b:B}P(b)} \pi x = f(a) @>>> \Sigma_{b:B} P(B)\\ @VVV @VVV \\ A @>{f}>> B \end{CD}$$ it a homotopy pullback square. Note, that using the induction principal for $\Sigma$-types it is easy to constructed the homotopy that makes this square homotopy commute. 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_{x : \Sigma_{b : B}P(b)} \pi x = f(a) $$ and homotopies making the obvious diagram commute upto homotopy. Infact, 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 infact a homotopy pullback square. I worked all of this out explicitly this morning. It is a good exercise in working inside HoTT, so i wont spoil it for anyone else who is 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 $.

$\endgroup$

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.