Homotopy equivalences are equivalences: take 3 | Homotopy Type Theory

Homotopy equivalences are equivalences: take 3

A basic fact in homotopy type theory is that homotopy equivalences are (coherent) equivalences. This is important because on the one hand, homotopy equivalences are the “correct” sort of equivalence, but on the other hand, for a function f the type of “homotopy equivalence data for f” is not an h-proposition. There are at least three definitions of “equivalence” which do give an h-proposition (assuming function extensionality) and are all equivalent:

• Voevodsky’s definition: all homotopy fibers are contractible.
• Adjoint equivalences: the two homotopies in a homotopy equivalence are compatible with one higher homotopy.
• h-isomorphisms: a homotopy section and a homotopy retraction.

Of these, the first two require more data than a homotopy equivalence. So in practice, when proving some map to be an equivalence, we want to be able to just show that it is a homotopy equivalence. Thus we need some way to recover that extra data if we are just given a homotopy equivalence.

(The third definition, h-isomorphisms, requires less data than a homotopy equivalence (the section and retraction don’t need to be the same, a priori), but as far as I know, showing that this definition gives an h-proposition is no easier than showing that every homotopy equivalence is a Voevodsky equivalence.)

Voevodsky’s proof that every homotopy equivalence is a (Voevodsky) equivalence shows that the homotopy fiber of f is a retract of a homotopy fiber of gf, while gf is an equivalence since it is homotopic to the identity. On the other hand, the proof currently in the HoTT repository uses a different approach motivated by higher category theory: we show that every homotopy equivalence can be “rectified” to an adjoint equivalence by changing one of the homotopies, and then from there we have essentially the data to make a Voevodsky equivalence after massaging it a bit.

I want to present a third approach to this fundamental theorem, which is motivated more by model category theory. Recall that a dependent type in type theory corresponds to a fibration in a model category. To say that each is contractible (with contraction varying continuously in x, as always) is equivalently to say that the projection p admits a (strict) section, s say, such that the composite is fiberwise homotopic to the identity. In this case we may say that s is a deformation section of p.

Now given any map , the dependent type represents the “mapping path fibration” which occurs in the (acyclic cofibration, fibration) factorization of f. (This is how Gambino and Garner constructed the identity type weak factorization system.) Therefore, to say that f is a Voevodsky equivalence is equivalently to say that the fibration part of this factorization has a deformation section, as above.

However, it’s easy to show that homotopy equivalences have the 2-out-of-3 property, and that every acyclic cofibration is a homotopy equivalence (in fact, it has a deformation retraction; Gambino and Garner showed this as well). Thus, if f is a homotopy equivalence, so is its mapping path fibration. Therefore, to show that any homotopy equivalence is a Voevodsky equivalence, it suffices to prove that a fibration which is a homotopy equivalence has a deformation section.

Using the path-lifting property of a fibration, it’s easy to modify a homotopy inverse to a fibration to become a strict section of it. Thus all that remains is to modify the one remaining homotopy to become fiberwise, which we can do by concatenating it with the inverse of . This is a degenerate case of “adjointification” when one of the homotopies is constant, but I think it is significantly simpler to understand than the general case. In particular, it avoids the confusing “play with naturality” bit (which is most comprehensible when written with string diagrams, and probably least comprehensible when written in terms that Coq can understand). It’s also the same way that the corresponding fact is proven in homotopy theory; see e.g. Prop. 7.8.2 in Hirschhorn’s book on model categories.

An implementation of this third proof in Coq is here. Once you take into account that it simplifies the later proofs of 2-out-of-3 for Voevodsky equivalences, I think it comes out to be a little bit shorter than the adjointification proof.