### 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) “$f\colon X\to Y$ is an equivalence” was defined as

$IsEquiv(f) \coloneqq \Pi_{y\in Y} IsContr( Fiber(f,y))$

where $Fiber(f,y) \coloneqq \Sigma_{x\in X} Paths_Y(f(x),y)$. I claimed that this is equivalent to the following type (which I didn’t write down in gory detail before):

$IsAdjointEquiv(f) \coloneqq \Sigma_{g\colon Y\to X} \Sigma_{p\in \Pi_{x\in X} Paths_X(g(f(x)),x)} \Sigma_{q\in \Pi_{y\in Y} Paths_Y(f(g(y)),y)} \Pi_{x\in X} Paths_{Paths_Y(f(g(f(x))),f(x))}(f(p(x)),q(f(x))).$

Ugh! If you unravel this, it means that a point of $IsAdjointEquiv(f)$ consists of:

- a map $g\colon Y\to X$,
- a “homotopy” $p\colon g\circ f\simeq 1_X$,
- a “homotopy” $q\colon f\circ g\simeq 1_Y$, and
- a “higher homotopy” $t\colon f(p) \simeq q_f$.

If all of our types were 1-types, i.e. groupoids, then this would be exactly an adjoint equivalence of groupoids: the two homotopies $p$ and $q$ 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 $IsEquiv(f)$. This consists of, for every $y\in Y$, a point of $IsContr( Fiber(f,y))$. The latter consists of a point of $Fiber(f,y)$ together with a contraction to that point. Now a point of $Fiber(f,y)$ consists of a point of $X$ along with a path from $f$ of that point to $y$. Call this point $g(y)$ and the path $q_y\in Paths_Y(f(g(y)),y)$. In this way we extract our map $g$ and homotopy $q$.

What remains in the data is the contraction of $Fiber(f,y)$ to $(g(y),q_y)$. This consists of, for every point $(x,r\colon f(x) \simeq y)$ of $Fiber(f,y)$, a path from $(x,r)$ to $(g(y),q_y)$. Now $Fiber(f,y)$ is the total space of a “fibration” (i.e. dependent type) over $X$, whose fiber over $x\in X$ is $Paths_Y(f(x),y)$—and so a path $(x,r)\simeq (g(y),q_y)$ in $Fiber(f,y)$ is determined by a path $a\colon x\simeq g(y)$ in the base space $X$, together with a path $b$ in the fiber $Paths_Y(f(g(y)),y)$ from $a_\ast(r)$ to $q_y$, where $a_\ast$ denotes fiber transport along the path $a$. But fiber transport in the fibration of paths is just composition of paths, so the latter is a homotopy from $r\circ f(a^{-1})$ to $q_y$.

Now consider, for any $x\in X$, the point $(x,1_{f(x)})\in Fiber(f,f(x))$. Then the path $a$ above can be called $p_x^{-1}\colon x \simeq g(f(x))$, and $b$ goes from $1_{f(x)} \circ f(p_x) \simeq f(p_x)$ to $q_{f(x)}$. So we obtain exactly the data of a point of $IsAdjointEquiv(f)$.

Conversely, the data of $g$ and $q$ in a point of $IsAdjointEquiv(f)$ is exactly what we need to specify, for every $y\in Y$, a point of $Fiber(f,y)$ (which is to say, a point of $\Pi_{y\in Y} Fiber(f,y)$). For the rest, given any $(x,r)$ in $Fiber(f,y)$, we can take $a$ to be $g(r) \circ p_x^{-1}$, and the remaining homotopy to be $r \circ f(p_x \circ g(r^{-1})) \simeq r\circ f(p_x) \circ f(g(r^{-1})) \overset{t}{\simeq} r \circ q_{f(x)} \circ f(g(r^{-1})) \simeq q_{y} \circ f(g(r)) \circ f(g(r^{-1})) \simeq q_{y}.$

This gives us maps in both directions between $IsEquiv(f)$ and $IsAdjointEquiv(f)$. (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 $IsEquiv(f)$ is a (-1)-type, if $IsAdjointEquiv(f)$ 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 $IsAdjointEquiv(f)$ 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 $t$, as not giving rise to a (-1)-type. If written out explicitly, this type would be

$IncoherentEquiv(f) \coloneqq \Sigma_{g\colon Y\to X}\; ( \Pi_{x\in X} Paths_X(g(f(x)),x) ) \; \times \; ( \Pi_{y\in Y} Paths_Y(f(g(y)),y) )$

However, perhaps I didn’t emphasize enough that as soon as $f\colon X\to Y$ admits *some* choice of “homotopy equivalence data” (i.e. $IncoherentEquiv(f)$ is inhabited) then $f$ is necessarily an equivalence in either of the above “coherent senses.” In fact, we can construct a map $IncoherentEquiv(f) \to IsAdjointEquiv(f)$ 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
$\Omega_x X \coloneqq Paths_X(x,x).$
So if we had an operation “$\pi_0$” or “$\tau_{\le 0}$” which reflects types into sets (i.e. 0-types), then we could define a *set* $\pi_n(X,x) \coloneqq \pi_0 (\Omega_x^n X)$ for any type $X$. (This is the internal-language version of categorical homotopy groups in an $(\infty,1)$-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 $\pi_n$, for all $n$ and all basepoints.

The quantifier “for all basepoints” means that $\pi_n$ should really be not just a single set, but a set indexed by $X$. And the quantifer “for all $n$” 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 $\pi_0$, 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 $(\infty,1)$-category of *all* topological spaces is a pretty weird beast by $(\infty,1)$-categorical standards, although it contains as a full sub-$(\infty,1)$-category the prototypical $(\infty,1)$-category of $\infty$-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
$(\infty,1)$-topoi*, and this isn’t really the time to talk more about them, except to say that they include many $(\infty,1)$-topoi of interest, including (in general) $\infty$-sheaves on topological spaces. Moreover, as $(\infty,1)$-topoi, they have all the other good properties we might ask of an $(\infty,1)$-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 $(\infty,1)$-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 $\infty$. But once I got over being sad about losing Whitehead’s theorem, I got excited that the $\infty$-categorical world has displayed to us this new structure, which was totally invisible to the $n$-categorical world for all finite $n$.

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 $\infty$-groupoids out of sets, then we will automatically be forced to accept Whitehead’s theorem; but if instead we define sets as particular $\infty$-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 $\Pi x:X\, \mathrm{Id}_{X}(g(f(x)),x)$ and $\mathrm{Id}_{X^X}(g\circ f,1_X)$. 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” $p:g\circ f \simeq 1_X$” – 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.