8.6 The Freudenthal suspension theorem

Before proving the Freudenthal suspension theorem, we need some auxiliary lemmas about connectedness. In \autorefcha:hlevels we proved a number of facts about n-connected maps and n-types for fixed n; here we are now interested in what happens when we vary n. For instance, in \autorefprop:nconnected_tested_by_lv_n_dependent types we showed that n-connected maps are characterized by an “inductionMathworldPlanetmath principle” relative to families of n-types. If we want to “induct along” an n-connected map into a family of k-types for k>n, we don’t immediately know that there is a function by such an induction principle, but the following lemma says that at least our ignorance can be quantified.

Lemma 8.6.1.

If f:AB is n-connected and P:Bk-Type is a family of k-types for kn, then the induced function


is (k-n-2)-truncated.


We induct on the natural numberMathworldPlanetmath k-n. When k=n, this is \autorefprop:nconnected_tested_by_lv_n_dependent types. For the inductive step, suppose f is n-connected and P is a family of k+1-types. To show that (f) is (k-n-1)-truncated, let k:(a:A)P(a); then we have


Let (g,p) and (h,q) lie in this type, so p:gfk and q:hfk; then we also have


However, here the right-hand side is a fiber of the map


where Q(b):(g(b)=h(b)). Since P is a family of (k+1)-types, Q is a family of k-types, so the inductive hypothesis implies that this fiber is a (k-n-2)-type. Thus, all path spaces of 𝖿𝗂𝖻(f)(k) are (k-n-2)-types, so it is a (k-n-1)-type. ∎

Recall that if (A,a0) and (B,b0) are pointed types, then their wedge AB is defined to be the pushout of Aa0𝟏b0B. There is a canonical map i:ABA×B defined by the two maps λa.(a,b0) and λb.(a0,b); the following lemma essentially says that this map is highly connected if A and B are so. It is a bit more convenient both to prove and use, however, if we use the characterizationMathworldPlanetmath of connectedness from \autorefprop:nconnected_tested_by_lv_n_dependent types and substitute in the universal propertyMathworldPlanetmath of the wedge (generalized to type families).

Lemma 8.6.2 (Wedge connectivity lemma).

Suppose that (A,a0) and (B,b0) are n- and m-connected pointed types, respectively, with n,m0, and let P:AB(n+m)-Type. Then for any f:(a:A)P(a,b0) and g:(b:B)P(a0,b) with p:f(a0)=g(b0), there exists h:(a:A)(b:B)P(a,b) with homotopiesMathworldPlanetmath

q:a:Ah(a,b0)=f(a)  𝑎𝑛𝑑  r:b:Bh(a0,b)=g(b)

such that p=q(a0)-1\centerdotr(b0).


Define P:A𝒰 by


Then we have (g,p):P(a0). Since a0:𝟏A is (n-1)-connected, if P is a family of (n-1)-types then we will have :(a:A)P(a) such that (a0)=(g,p), in which case we can define h(a,b):𝗉𝗋1((a))(b). However, for fixed a, the type P(a) is the fiber over f(a) of the map


given by precomposition with b0:𝟏B. Since b0:𝟏B is (m-1)-connected, for this fiber to be (n-1)-connected, by \autorefthm:conn-trunc-variable-ind it suffices for each type P(a,b) to be an (n+m)-type, which we have assumed. ∎

Let (X,x0) be a pointed type, and recall the definition of the suspensionMathworldPlanetmath ΣX from \autorefsec:suspension, with constructors 𝖭,𝖲:ΣX and 𝗆𝖾𝗋𝗂𝖽:X(𝖭=𝖲). We regard ΣX as a pointed space with basepoint 𝖭, so that we have ΩΣX:(𝖭=ΣX𝖭). Then there is a canonical map

σ(x) :𝗆𝖾𝗋𝗂𝖽(x)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1.
Remark 8.6.3.

In classical algebraic topology, one considers the reduced suspension, in which the path merid(x0) is collapsed down to a point, identifying N and S. The reduced and unreduced suspensions are homotopy equivalent, so the distinction is invisible to our purely homotopy-theoretic eyes — and higher inductive types only allow us to “identify” points up to a higher path anyway, there is no purpose to considering reduced suspensions in homotopy type theory. However, the “unreducedness” of our suspension is the reason for the (possibly unexpected) appearance of merid(x0)-1 in the definition of σ.

Our goal is now to prove the following.

Theorem 8.6.4 (The Freudenthal suspension theorem).

Suppose that X is n-connected and pointed, with n0. Then the map σ:XΩΣ(X) is 2n-connected.

We will use the encode-decode method, but applied in a slightly different way. In most cases so far, we have used it to characterize the loop spaceMathworldPlanetmath Ω(A,a0) of some type as equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to some other type B, by constructing a family 𝖼𝗈𝖽𝖾:A𝒰 with 𝖼𝗈𝖽𝖾(a0):B and a family of equivalences 𝖽𝖾𝖼𝗈𝖽𝖾:(x:A)𝖼𝗈𝖽𝖾(x)(a0=x).

In this case, however, we want to show that σ:XΩΣX is 2n-connected. We could use a truncated version of the previous method, such as we will see in \autorefsec:van-kampen, to prove that X2nΩΣX2n is an equivalence—but this is a slightly weaker statement than the map being 2n-connected (see \autorefthm:conn-pik,\autorefthm:pik-conn). However, note that in the general case, to prove that 𝖽𝖾𝖼𝗈𝖽𝖾(x) is an equivalence, we could equivalently be proving that its fibers are contractibleMathworldPlanetmath, and we would still be able to use induction over the base type. This we can generalize to prove connectedness of a map into a loop space, i.e. that the truncationsMathworldPlanetmath of its fibers are contractible. Moreover, instead of constructing 𝖼𝗈𝖽𝖾 and 𝖽𝖾𝖼𝗈𝖽𝖾 separately, we can construct directly a family of codes for the truncations of the fibers.

Definition 8.6.5.

If X is n-connected and pointed with n0, then there is a family

𝖼𝗈𝖽𝖾:y:ΣX(𝖭=y)𝒰 (8.6.5)

such that

𝖼𝗈𝖽𝖾(𝖭,p) :𝖿𝗂𝖻σ(p)2n(x:X)(𝗆𝖾𝗋𝗂𝖽(x)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1=p)2n (8.6.6)
𝖼𝗈𝖽𝖾(𝖲,q) :𝖿𝗂𝖻𝗆𝖾𝗋𝗂𝖽(q)2n(x:X)(𝗆𝖾𝗋𝗂𝖽(x)=q)2n. (8.6.6)

Our eventual goal will be to prove that 𝖼𝗈𝖽𝖾(y,p) is contractible for all y:ΣX and p:𝖭=y. Applying this with y:𝖭 will show that all fibers of σ are 2n-connected, and thus σ is 2n-connected.

Proof of \autorefthm:freudcode.

We define 𝖼𝗈𝖽𝖾(y,p) by induction on y:ΣX, where the first two cases are (8.6.6) and (8.6.6). It remains to construct, for each x1:X, a dependent path


By \autorefthm:dpath-arrow, this is equivalent to giving a family of paths


And by univalence and transport in path types, this is equivalent to a family of equivalences


We will define a family of maps

q:𝖭=𝖲𝖼𝗈𝖽𝖾(𝖭,q\centerdot𝗆𝖾𝗋𝗂𝖽(x1)-1)𝖼𝗈𝖽𝖾(𝖲,q). (8.6.7)

and then show that they are all equivalences. Thus, let q:𝖭=𝖲; by the universal property of truncation and the definitions of 𝖼𝗈𝖽𝖾(𝖭,) and 𝖼𝗈𝖽𝖾(𝖲,), it will suffice to define for each x2:X, a map


Now for each x1,x2:X, this type is 2n-truncated, while X is n-connected. Thus, by \autorefthm:wedge-connectivity, it suffices to define this map when x1 is x0, when x2 is x0, and check that they agree when both are x0.

When x1 is x0, the hypothesisMathworldPlanetmathPlanetmath is r:𝗆𝖾𝗋𝗂𝖽(x2)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1=q\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1. Thus, by canceling 𝗆𝖾𝗋𝗂𝖽(x0)-1 from r to get r:𝗆𝖾𝗋𝗂𝖽(x2)=q, so we can define the image to be |(x2,r)|2n.

When x2 is x0, the hypothesis is r:𝗆𝖾𝗋𝗂𝖽(x0)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1=q\centerdot𝗆𝖾𝗋𝗂𝖽(x1)-1. Rearranging this, we obtain r′′:𝗆𝖾𝗋𝗂𝖽(x1)=q, and we can define the image to be |(x1,r′′)|2n.

Finally, when both x1 and x2 are x0, it suffices to show the resulting r and r′′ agree; this is an easy lemma about path composition. This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the definition of (8.6.7). To show that it is a family of equivalences, since being an equivalence is a mere proposition and x0:𝟏X is (at least) (-1)-connected, it suffices to assume x1 is x0. In this case, inspecting the above construction we see that it is essentially the 2n-truncation of the function that cancels 𝗆𝖾𝗋𝗂𝖽(x0)-1, which is an equivalence. ∎

In additionPlanetmathPlanetmath to (8.6.6) and (8.6.6), we will need to extract from the construction of 𝖼𝗈𝖽𝖾 some information about how it acts on paths. For this we use the following lemma.

Lemma 8.6.8.

Let A:U, B:AU, and C:(a:A)B(a)U, and also a1,a2:A with m:a1=a2 and b:B(a2). Then the function


where t:transportB(m,transportB(m-1,b))=b is the obvious coherence path and C^:((a:A)B(a))U is the uncurried form of C, is equal to the equivalence obtained by univalence from the composite

C(a1,𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B(m-1,b)) =𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍λa.B(a)𝒰(m,C(a1))(b) (by \eqref{eq:transport-arrow})
=C(a2,b). (by $\mathsf{happly}(\mathsf{apd}_{C}\mathopen{}\left(m\right)\mathclose{},b)$)

By path induction, we may assume a2 is a1 and m is 𝗋𝖾𝖿𝗅a1, in which case both functions are the identityPlanetmathPlanetmathPlanetmath. ∎

We apply this lemma with A:ΣX and B:λy.(𝖭=y) and C:𝖼𝗈𝖽𝖾, while a1:𝖭 and a2:𝖲 and m:𝗆𝖾𝗋𝗂𝖽(x1) for some x1:X, and finally b:q is some path 𝖭=𝖲. The computation rule for induction over ΣX identifies 𝖺𝗉𝖽C(m) with a path constructed in a certain way out of univalence and function extensionality. The second function described in \autorefthm:freudlemma essentially consists of undoing these applications of univalence and function extensionality, reducing back to the particular functions (8.6.7) that we defined using \autorefthm:wedge-connectivity. Therefore, \autorefthm:freudlemma says that transporting along 𝗉𝖺𝗂𝗋=(q,t) essentially recovers these functions.

Finally, by construction, when x1 or x2 coincides with x0 and the input is in the image of ||2n, we know more explicitly what these functions are. Thus, for any x2:X, we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝖽𝖾^(𝗉𝖺𝗂𝗋=(𝗆𝖾𝗋𝗂𝖽(x0),t),|(x2,r)|2n)=|(x1,r)|2n (8.6.9)

where r:𝗆𝖾𝗋𝗂𝖽(x2)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B(𝗆𝖾𝗋𝗂𝖽(x0)-1,q) is arbitrary as before, and r:𝗆𝖾𝗋𝗂𝖽(x2)=q is obtained from r by identifying its end pointPlanetmathPlanetmath with q\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1 and canceling 𝗆𝖾𝗋𝗂𝖽(x0)-1. Similarly, for any x1:X, we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝖽𝖾^(𝗉𝖺𝗂𝗋=(𝗆𝖾𝗋𝗂𝖽(x1),t),|(x0,r)|2n)=|(x1,r′′)|2n (8.6.10)

where r:𝗆𝖾𝗋𝗂𝖽(x0)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B(𝗆𝖾𝗋𝗂𝖽(x1)-1,q), and r′′:𝗆𝖾𝗋𝗂𝖽(x1)=q is obtained by identifying its end point and rearranging paths.

Proof of \autorefthm:freudenthal.

It remains to show that 𝖼𝗈𝖽𝖾(y,p) is contractible for each y:ΣX and p:𝖭=y. First we must choose a center of contraction, say c(y,p):𝖼𝗈𝖽𝖾(y,p). This corresponds to the definition of the function 𝖾𝗇𝖼𝗈𝖽𝖾 in our previous proofs, so we define it by transport. Note that in the special case when y is 𝖭 and p is 𝗋𝖾𝖿𝗅𝖭, we have


Thus, we can choose c(𝖭,𝗋𝖾𝖿𝗅𝖭):|(x0,𝗋𝗂𝗇𝗏𝗆𝖾𝗋𝗂𝖽(x0))|2n, where rinvq is the obvious path q\centerdotq-1=𝗋𝖾𝖿𝗅 for any q. We can now obtain c:(y:ΣX)(p:𝖭=y)𝖼𝗈𝖽𝖾(y,p) by path induction on p, but it will be important below that we can also give a concrete definition in terms of transport:


where 𝖼𝗈𝖽𝖾^:((y:ΣX)(𝖭=y))𝒰 is the uncurried version of 𝖼𝗈𝖽𝖾, and 𝗍𝗂𝖽p:p*(𝗋𝖾𝖿𝗅)=p is a standard lemma.

Next, we must show that every element of 𝖼𝗈𝖽𝖾(y,p) is equal to c(y,p). Again, by path induction, it suffices to assume y is 𝖭 and p is 𝗋𝖾𝖿𝗅𝖭. In fact, we will prove it more generally when y is 𝖭 and p is arbitrary. That is, we will show that for any p:𝖭=𝖭 and d:𝖼𝗈𝖽𝖾(𝖭,p) we have d=c(𝖭,p). Since this equality is a (2n-1)-type, we may assume d is of the form |(x1,r)|2n for some x1:X and r:𝗆𝖾𝗋𝗂𝖽(x1)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1=p.

Now by a further path induction, we may assume that r is reflexivityMathworldPlanetmath, and p is 𝗆𝖾𝗋𝗂𝖽(x1)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1. (This is why we generalized to arbitrary p above.) Thus, we have to prove that

|(x1,𝗋𝖾𝖿𝗅𝗆𝖾𝗋𝗂𝖽(x1)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1)|2n=c(𝖭,𝗋𝖾𝖿𝗅𝗆𝖾𝗋𝗂𝖽(x1)\centerdot𝗆𝖾𝗋𝗂𝖽(x0)-1). (8.6.11)

By definition, the right-hand side of this equality is


where the underscore ¯ ought to be filled in with suitable coherence paths. Here the first step is functoriality of transport, the second invokes (8.6.10), and the third invokes (8.6.9) (with transport moved to the other side). Thus we have the same first component as the left-hand side of (8.6.11). We leave it to the reader to verify that the coherence paths all cancel, giving reflexivity in the second component. ∎

Corollary 8.6.12 (Freudenthal Equivalence).

Suppose that X is n-connected and pointed, with n0. Then X2nΩΣ(X)2n.


By \crefthm:freudenthal, σ is 2n-connected. By \creflem:connected-map-equiv-truncation, it is therefore an equivalence on 2n-truncations. ∎

One important corollary of the Freudenthal suspension theorem is that the homotopy groups of spheres are stable in a certain range (these are the northeast-to-southwest diagonals in \autoreftab:homotopy-groups-of-spheres):

Corollary 8.6.13 (Stability for Spheres).

If k2n-2, then πk+1(Sn+1)=πk(Sn).


Assume k2n-2. By \crefcor:sn-connected, 𝕊n is (n-1)-connected. Therefore, by \crefcor:freudenthal-equiv,


By \creflem:truncation-le, because k2(n-1), applying k to both sides shows that this equation holds for k:

Ω(Σ(𝕊n))k=𝕊nk. (8.6.14)

Then, the main idea of the proof is as follows; we omit checking that these equivalences act appropriately on the base points of these spaces:

πk+1(𝕊n+1) Ωk+1(𝕊n+1)0
=Ωk((Ω(Σ(𝕊n)))k) (by \autorefthm:path-truncation)
=Ωk(𝕊nk) (by \eqref{eq:freudenthal-for-spheres})
=Ωk(𝕊n)0 (by \autorefthm:path-truncation)

This means that once we have calculated one entry in one of these stable diagonals, we know all of them. For example:

Theorem 8.6.15.

πn(𝕊n)= for every n1.


The proof is by induction on n. We already have π1(𝕊1)= (\autorefcor:pi1s1) and π2(𝕊2)= (\autorefcor:pis2-hopf). When n2, n(2n-2). Therefore, by \crefcor:stability-spheres, πn+1(Sn+1)=πn(Sn), and this equivalence, combined with the inductive hypothesis, gives the result. ∎

Corollary 8.6.16.

𝕊n+1 is not an n-type for any n-1.

Title 8.6 The Freudenthal suspension theorem