Homotopy Type Theory, III
Posted by Mike Shulman
It’s a dangerous business making promises about what will happen “next time” when I don’t have “next time” written yet. I said last time that I intended to talk about the univalence axiom next, but then I realized there is more I want to say about equivalences first, and perhaps functional extensionality.
But before I get into that, I’d like to mention that Steve Awodey has written a very nice post about intensional type theory and its relation to homotopy type theory from an intensional type theorists’ point of view; read it at the HoTT blog!
Now, recall that the proposition (that is, the (-1)-type) “ is an equivalence” was defined as
where . I claimed that this is equivalent to the following type (which I didn’t write down in gory detail before):
Ugh! If you unravel this, it means that a point of consists of:
- a map ,
- a “homotopy” ,
- a “homotopy” , and
- a “higher homotopy” .
If all of our types were 1-types, i.e. groupoids, then this would be exactly an adjoint equivalence of groupoids: the two homotopies and are the unit and counit, and the higher homotopy asserts one triangle identity. The other triangle identity then follows; see the nLab page.
I didn’t really say anything about why these types should be equivalent, though. Suppose that we have a point of . This consists of, for every , a point of . The latter consists of a point of together with a contraction to that point. Now a point of consists of a point of along with a path from of that point to . Call this point and the path . In this way we extract our map and homotopy .
What remains in the data is the contraction of to . This consists of, for every point of , a path from to . Now is the total space of a “fibration” (i.e. dependent type) over , whose fiber over is —and so a path in is determined by a path in the base space , together with a path in the fiber from to , where denotes fiber transport along the path . But fiber transport in the fibration of paths is just composition of paths, so the latter is a homotopy from to .
Now consider, for any , the point . Then the path above can be called , and goes from to . So we obtain exactly the data of a point of .
Conversely, the data of and in a point of is exactly what we need to specify, for every , a point of (which is to say, a point of ). For the rest, given any in , we can take to be , and the remaining homotopy to be
This gives us maps in both directions between and . (Note that because all the above manipulations are completely formulaic, they formalize directly into type-theoretic constructions. I’m sure of this, because I’ve coded both of these maps in Coq, using Andrej Bauer’s convenient “tactics”—maybe I’ll get around to talking about Coq in a later post. In particular, operations such as composing and inverting paths, and acting on them by functions, are easily definable in terms of the rules for identity types that I mentioned in the first post.)
Thus, if either of the two types above is inhabited, so is the other. Ideally, we’d like them to actually be equivalent. Since is a (-1)-type, if were also a (-1)-type, having morphisms in both directions would be enough for them to be equivalent. Or we could also try to enrich the above two maps into an (adjoint) equivalence, which would then imply that is a (-1)-type. I haven’t managed to get either of these approaches to work in Coq yet, but I believe that it should be true. (We will need to use functional extensionality, since the points of these two types contain functions.)
Now recall also that I disparaged the naive notion of “homotopy equivalence” which lacks the higher homotopy , as not giving rise to a (-1)-type. If written out explicitly, this type would be
However, perhaps I didn’t emphasize enough that as soon as admits some choice of “homotopy equivalence data” (i.e. is inhabited) then is necessarily an equivalence in either of the above “coherent senses.” In fact, we can construct a map by copying the usual 2-categorical proof that any non-adjoint equivalence can be improved to an adjoint equivalence (by changing one of the natural isomorphisms). See the nLab page for a string diagram proof. Of course, in practice, this is often a convenient way to prove that a given map is an equivalence.
I also neglected to mention that Voevodsky currently refers to these equivalence as weak equivalences. I don’t, because as you can see there is nothing “weak” about them. Usually “weak” is prefixed to maps that we want to think of as equivalences, but which don’t necessarily admit inverses (even up to homotopy). But these equivalences do have homotopy inverses. (The term “h-isomorphism” was also proposed at Oberwolfach, but I prefer simply “equivalence.”)
One might ask, though, is there a notion of weak equivalence in homotopy type theory? In classical homotopy theory, we define a “weak homotopy equivalence” to be one inducing an isomorphism on all homotopy groups. Can we define homotopy groups in homotopy type theory?
We definitely have a notion of “based loop space” (or rather “based loop type”), namely So if we had an operation “” or “” which reflects types into sets (i.e. 0-types), then we could define a set for any type . (This is the internal-language version of categorical homotopy groups in an -topos.) And of course, when restricted to sets, the above notion of equivalence for types can be regarded as the familiar notion of isomorphism (= bijection). So we could define a “weak equivalence” to be a map inducing an isomorphism on , for all and all basepoints.
The quantifier “for all basepoints” means that should really be not just a single set, but a set indexed by . And the quantifer “for all ” here could be either in the metatheory or in the theory itself. But the more important point is that we shouldn’t expect to prove in homotopy type theory that every weak equivalence, in this sense, is an actual equivalence. In other words, “Whitehead’s theorem” should not be provable.
In fact, the fragment of the theory that I’ve described so far has a model in topological spaces—arbitrary topological spaces, not necessarily even of the homotopy type of CW complexes. (Probably; see this comment.) If this model has a , then Whitehead’s theorem will probably fail as usual for spaces that aren’t of the homotopy type of a CW complex. This model might lead you to think that the failure of Whitehead’s theorem is a bad thing: the -category of all topological spaces is a pretty weird beast by -categorical standards, although it contains as a full sub--category the prototypical -category of -groupoids (modeled by CW complexes).
But actually, there are also important, interesting, and otherwise well-behaved “homotopy theories” in which Whitehead’s theorem fails. I’m thinking of non-hypercomplete -topoi, and this isn’t really the time to talk more about them, except to say that they include many -topoi of interest, including (in general) -sheaves on topological spaces. Moreover, as -topoi, they have all the other good properties we might ask of an -category.
It took me a little while to come to terms with this. Now I think we can think of Whitehead’s theorem as a “classicality” axiom which can fail in -topoi, akin to the law of excluded middle and the axiom of choice (which can already fail in 1-topoi). It’s curious in that we don’t notice it until we go all the way to . But once I got over being sad about losing Whitehead’s theorem, I got excited that the -categorical world has displayed to us this new structure, which was totally invisible to the -categorical world for all finite .
Put another way, Whitehead’s theorem should be regarded as a foundational axiom of mathematics, but one which only a “natively homotopical” foundational system is subtle enough to perceive (and in particular, to allow to be violated). If we insist on building -groupoids out of sets, then we will automatically be forced to accept Whitehead’s theorem; but if instead we define sets as particular -groupoids, then we are allowed to explore a world where Whitehead’s theorem may fail.
Re: Homotopy Type Theory, III
another great posting full of things to think about and discuss! First, though, with respect to the definition of weak equivalence: without function extensionality (FE), there is of course a difference between and . So although you used the former (weaker) notion in the writing out the type IsAdjointEquiv(f), in the “unravelled” explanation that follows you said “a “homotopy” ” – which is maybe better formalized in the stronger way.
So, without FE there are indeed weak and strong notions of equivalence: roughly “pointwise equivalence”, and “intensional isomorphism”. Of course, Univalence collapses the difference.