homotopy equivalence


Homotopy theory

Equality and Equivalence



A homotopy equivalence between topological spaces (or other objects in a category equipped with a notion of homotopy) XX and YY is a morphism f:XYf:X\to Y which has a homotopy inverse, hence such that there exists a morphism g:YXg:Y\to X and homotopies gf1 Xg \circ f \sim 1_X and fg1 Yf \circ g \sim 1_Y.

(Note the similarity with the strict notion of equivalence of categories.)

If there exists a homotopy equivalence between XX and YY we say that XX and YY are homotopy equivalent or that they have the same homotopy type. Being homotopy equivalent is evidently an equivalence relation.

For many purposes, one wants instead weak homotopy equivalences. Often when speaking of a homotopy equivalence or a homotopy type, one actually means the weak version. (This is especially likely on this wiki, due to the relationship to \infty-infinity-groupoids suggested by the homotopy hypothesis.)


The homotopy category of Top with respect to homotopy equivalences is Ho(Top) he{}_{he}.

More generally, in any (∞,1)-category CC other than Top, a homotopy equivalence in CC is just an equivalence in CC.


Any homotopy equivalence is also a weak homotopy equivalence. Conversely, in the context of topological spaces, any weak homotopy equivalence between m-cofibrant spaces (spaces that are homotopy equivalent to CW complexes) is a homotopy equivalence. This is the Whitehead theorem.

The homotopy equivalences are the weak equivalences in the Strøm model structure on topological spaces. The homotopy category resulting from inverting all homotopy equivalences in Top is the same as that resulting from identifying homotopic maps.

Strong homotopy equivalences

Sometimes an apparently stronger form of homotopy equivalence is needed. These seem to have been first noticed by Richard Lashof in 1970 in work on triangulation and smoothing. The point is one of the interaction between the two homotopies, which are not made explicit in the definition above. Let us set this up slightly differently:

In a homotopy equivalence there are the two maps f:XYf: X\to Y and g:YXg: Y\to X, then two homotopies

H:X×IX,H:gf1 XH : X\times I \to X, H:g \circ f \sim 1_X


K:Y×IY,K:fg1 Y.K: Y\times I \to Y, K : f \circ g \sim 1_Y.

The whiskering actions of maps on homotopies (and more generally in any (∞,1)-category or category with a cylinder functor) gives two homotopies fgfff\circ g \circ f \sim f, namely f *H=fH:X×IYf_*H = f\circ H : X\times I \to Y and f *K=K(f×I)f^*K = K\circ (f\times I). Similarly, of course, there are two homotopies gfggg\circ f \circ g \sim g, namely g *Kg_*K and g *Hg^*H. In the usual definition of homotopy equivalence, there is no coherence required between these. That is handled precisely by the notion of stong homotopy equivalence. More precisely Lashof defined


A strong homotopy equivalence between spaces XX and YY is a quadruple (f,g,H,K)(f,g,H,K), as above, such that f *Hf *Kf_*H \sim f^*K and g *Kg *Hg_*K\sim g^*H.

Thus this imposes a minimal coherence condition on the data making up the homotopy equivalence. The definition clearly can be generalised to any reasonable setting with a notion of homotopy.

For example, in a 2-category where a homotopy is a natural isomorphism, and a homotopy between homotopies is just an equality, a homotopy equivalence is simply an equivalence, while a strong homotopy equivalence is the same as an adjoint equivalence.

The question naturally arises as to whether all homotopy equivalences are strong. Rainer Vogt(1972) proved

Vogt’s Lemma

If f:XYf: X\to Y be a morphism that is a homotopy equivalence in TopTop, let g:YXg: Y\to X be a homotopy inverse and H:gf1 XH:g \circ f \sim 1_X a homotopy. Then there is a homotopy K:fg1 YK: f \circ g \sim 1_Y such that (f,g,H,K)(f,g,H,K) is a strong homotopy equivalence.

Various versions of this are known in other settings, e.g. SSetSSet-enriched categories. In a 2-category the corresponding fact is that any equivalence can be improved to an adjoint equivalence, by changing at most one of the 2-cell isomorphisms involved.

Note, though, that the coherence supplied by Vogt’s lemma is not required to continue to higher levels. There is no condition of compatibilty between the two ‘homotopies between the homotopies’. In some situations, at least, some higher compatibility is known to be derivable; for instance, any biequivalence in a 3-category can be improved to an adjoint biequivalence.

Tim: I do not know if there is a neat formulation of the full homotopy coherent version of this, nor exactly in what settings the analogous abstract versions of Vogt’s lemma go across

Mike Shulman: I think there’s a “full coherentification” version for quasicategories in HTT somewhere.

Vogt’s Lemma plays a key role in the proof of Vogt’s theorem (cf. homotopy coherent diagrams).


Revised on May 4, 2016 06:42:56 by Urs Schreiber (