7.5 Connectedness

An n-type is one that has no interesting information above dimension n. By contrast, an n-connected type is one that has no interesting information below dimension n. It turns out to be natural to study a more general notion for functions as well.

Definition 7.5.1.

A function f:Aβ†’B is said to be n-connected if for all b:B, the type βˆ₯fibf⁒(b)βˆ₯n is contractibleMathworldPlanetmath:


A type A is said to be n-connected if the unique function Aβ†’1 is n-connected, i.e.Β if βˆ₯Aβˆ₯n is contractible.

Thus, a function f:Aβ†’B is n-connected if and only if 𝖿𝗂𝖻f⁒(b) is n-connected for every b:B. Of course, every function is (-2)-connected. At the next level, we have:

Lemma 7.5.2.

A function f is (-1)-connected if and only if it is surjectivePlanetmathPlanetmath in the sense of Β§4.6 (http://planetmath.org/46surjectionsandembeddings).


We defined f to be surjective if βˆ₯𝖿𝗂𝖻f⁒(b)βˆ₯-1 is inhabited for all b. But since it is a mere proposition, inhabitation is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to contractibility. ∎

Thus, n-connectedness of a function for nβ‰₯0 can be thought of as a strong form of surjectivity. Category-theoretically, (-1)-connectedness corresponds to essential surjectivity on objects, while n-connectedness corresponds to essential surjectivity on k-morphismsMathworldPlanetmathPlanetmath for k≀n+1.

Lemma 7.5.2 (http://planetmath.org/75connectedness#Thmprelem1) also implies that a type A is (-1)-connected if and only if it is merely inhabited. When a type is 0-connected we may simply say that it is connected, and when it is 1-connected we say it is simply connected.

Remark 7.5.3.

While our notion of n-connectedness for types agrees with the standard notion in homotopy theory, our notion of n-connectedness for functions is off by one from a common indexing in classical homotopy theory. Whereas we say a function f is n-connected if all its fibers are n-connected, some classical homotopyMathworldPlanetmathPlanetmath theorists would call such a function (n+1)-connected. (This is due to a historical focus on cofibers rather than fibers.)

We now observe a few closure properties of connected maps.

Lemma 7.5.4.

Suppose that g is a retract of a n-connected function f. Then g is n-connected.


This is a direct consequence of Lemma 4.7.3 (http://planetmath.org/47closurepropertiesofequivalences#Thmprelem1). ∎

Corollary 7.5.5.

If g is homotopicMathworldPlanetmath to a n-connected function f, then g is n-connected.

Lemma 7.5.6.

Suppose that f:Aβ†’B is n-connected. Then g:Bβ†’C is n-connected if and only if g∘f is n-connected.


For any c:C, we have

βˆ₯𝖿𝗂𝖻g∘f⁒(c)βˆ₯n ≃βˆ₯βˆ‘w:𝖿𝗂𝖻g⁒(c)𝖿𝗂𝖻f⁒(𝗉𝗋1⁒w)βˆ₯n (by http://planetmath.org/node/87774Exercise 4.4)
≃βˆ₯βˆ‘w:𝖿𝗂𝖻g⁒(c)βˆ₯𝖿𝗂𝖻f(𝗉𝗋1w)βˆ₯nβˆ₯n (by Theorem 7.3.9 (http://planetmath.org/73truncationshmprethm3))
≃βˆ₯𝖿𝗂𝖻g(c)βˆ₯n. (since $\mathopen{}\left\|{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)\right\|_{n}\mathclose{}$ is contractible)

It follows that βˆ₯𝖿𝗂𝖻g⁒(c)βˆ₯n is contractible if and only if βˆ₯𝖿𝗂𝖻g∘f⁒(c)βˆ₯n is contractible. ∎

Importantly, n-connected functions can be equivalently characterized as those which satisfy an β€œinductionMathworldPlanetmath principle” with respect to n-types. This idea will lead directly into our proof of the Freudenthal suspension theorem in Β§8.6 (http://planetmath.org/86thefreudenthalsuspensiontheorem).

Lemma 7.5.7.

For f:A→B and P:B→U, consider the following function:


For a fixed f and nβ‰₯-2, the following are equivalent.

  1. 1.

    f is n-connected.

  2. 2.

    For every P:Bβ†’n⁒-⁒𝖳𝗒𝗉𝖾, the map λ⁒s.s∘f is an equivalence.

  3. 3.

    For every P:Bβ†’n⁒-⁒𝖳𝗒𝗉𝖾, the map λ⁒s.s∘f has a sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath.


Suppose that f is n-connected and let P:Bβ†’n⁒-⁒𝖳𝗒𝗉𝖾. Then we have the equivalences

∏b:BP⁒(b) β‰ƒβˆb:B(βˆ₯𝖿𝗂𝖻f(b)βˆ₯nβ†’P(b)) (since $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}$ is contractible)
β‰ƒβˆb:B(𝖿𝗂𝖻f(b)β†’P(b)) (since $P(b)$ is an $n$-type)
β‰ƒβˆ(b:B)∏(a:A)∏(p:f(a)=b)P⁒(b) (by the left universal propertyMathworldPlanetmath of $\Sigma$-types)
β‰ƒβˆa:AP⁒(f⁒(a)). (by the left universal property of path types)

We omit the proof that this equivalence is indeed given by λ⁒s.s∘f. Thus,Β 1β‡’2, and clearlyΒ 2β‡’3. To showΒ 3β‡’1, consider the type family


ThenΒ 3 yields a map c:∏(b:B)βˆ₯𝖿𝗂𝖻f(b)βˆ₯n with c(f(a))=|(a,𝗋𝖾𝖿𝗅f⁒(a))|n. To show that each βˆ₯𝖿𝗂𝖻f⁒(b)βˆ₯n is contractible, we will find a function of type


By Theorem 7.3.2 (http://planetmath.org/73truncations#Thmprethm1), for this it suffices to find a function of type


But by rearranging variables and path induction, this is equivalent to the type


This property holds by our choice of c⁒(f⁒(a)). ∎

Corollary 7.5.8.

For any A, the canonical function |–|n:Aβ†’βˆ₯Aβˆ₯n is n-connected.


By Theorem 7.3.2 (http://planetmath.org/73truncations#Thmprethm1) and the associated uniqueness principle, the condition of Lemma 7.5.7 (http://planetmath.org/75connectedness#Thmprelem4) holds. ∎

For instance, when n=-1, Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2) says that the map Aβ†’βˆ₯Aβˆ₯ from a type to its propositional truncation is surjective.

Corollary 7.5.9.

A type A is n-connected if and only if the map


is an equivalence for every n-type B. In other words, β€œevery map from A to an n-type is constant”.


By Lemma 7.5.7 (http://planetmath.org/75connectedness#Thmprelem4) applied to a function with codomain 𝟏. ∎

Lemma 7.5.10.

Let B be an n-type and let f:Aβ†’B be a function. Then the induced function g:βˆ₯Aβˆ₯nβ†’B is an equivalence if and only if f is n-connected.


By Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2), |–|n is n-connected. Thus, since f=g∘|–|n, by Lemma 7.5.6 (http://planetmath.org/75connectedness#Thmprelem3) f is n-connected if and only if g is n-connected. But since g is a function between n-types, its fibers are also n-types. Thus, g is n-connected if and only if it is an equivalence. ∎

We can also characterize connected pointed types in terms of connectivity of the inclusion of their basepoint.

Lemma 7.5.11.

Let A be a type and a0:1β†’A a basepoint, with nβ‰₯-1. Then A is n-connected if and only if the map a0 is (n-1)-connected.


First suppose a0:πŸβ†’A is (n-1)-connected and let B be an n-type; we will use Corollary 7.5.9 (http://planetmath.org/75connectedness#Thmprecor3). The map Ξ»b.Ξ»a.b:Bβ†’(Aβ†’B) has a retraction given by f↦f⁒(a0), so it suffices to show it also has a section, i.e.Β that for any f:Aβ†’B there is b:B such that f=λ⁒a.b. We choose b:≑f(a0). Define P:A→𝒰 by P(a):≑(f(a)=f(a0)). Then P is a family of (n-1)-types and we have P⁒(a0); hence we have ∏(a:A)P⁒(a) since a0:πŸβ†’A is (n-1)-connected. Thus, f=λ⁒a.f⁒(a0) as desired.

Now suppose A is n-connected, and let P:Aβ†’(n-1)⁒-⁒𝖳𝗒𝗉𝖾 and u:P⁒(a0) be given. By Lemma 7.5.7 (http://planetmath.org/75connectedness#Thmprelem4), it will suffice to construct f:∏(a:A)P⁒(a) such that f⁒(a0)=u. Now (n-1)⁒-⁒𝖳𝗒𝗉𝖾 is an n-type and A is n-connected, so by Corollary 7.5.9 (http://planetmath.org/75connectedness#Thmprecor3), there is an n-type B such that P=λ⁒a.B. Hence, we have a family of equivalences g:∏(a:A)(P(a)≃B). Define f(a):≑ga-1(ga0(u)); then f:∏(a:A)P⁒(a) and f⁒(a0)=u as desired. ∎

In particular, a pointed type (A,a0) is 0-connected if and only if a0:πŸβ†’A is surjective, which is to say ∏(x:A)βˆ₯x=a0βˆ₯.

A useful variation on Lemma 7.5.6 (http://planetmath.org/75connectedness#Thmprelem3) is:

Lemma 7.5.12.

Let f:Aβ†’B be a function and P:Aβ†’U and Q:Bβ†’U be type families. Suppose that g:∏(a:A)P⁒(a)β†’Q⁒(f⁒(a)) is a fiberwise n-connected family of functions, i.e.Β each function ga:P⁒(a)β†’Q⁒(f⁒(a)) is n-connected. Then the function

Ο† :(βˆ‘a:AP⁒(a))β†’(βˆ‘b:BQ⁒(b))
φ⁒(a,u) :≑(f(a),ga(u))

is n-connected if and only if f is n-connected.


For b:B and v:Q⁒(b) we have

βˆ₯𝖿𝗂𝖻φ((b,v))βˆ₯n ≃βˆ₯βˆ‘(a:A)βˆ‘(u:P(a))βˆ‘(p:f(a)=b)f(p)*(ga(u))=vβˆ₯n

where the transportations along f⁒(p) and f⁒(p)-1 are with respect to Q. Therefore, if either is contractible, so is the other. ∎

In the other direction, we have

Lemma 7.5.13.

Let P,Q:A→U be type families and consider a fiberwise transformationPlanetmathPlanetmath


from P to Q. Then the induced map total⁒(f):βˆ‘(a:A)P⁒(a)β†’βˆ‘(a:A)Q⁒(a) is n-connected if and only if each f⁒(a) is n-connected.


By Theorem 4.7.6 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm3), we have π–Ώπ—‚π–»π—π—ˆπ—π–Ίπ—…β’(f)((x,v))≃𝖿𝗂𝖻f⁒(x)(v) for each x:A and v:Q⁒(x). Hence βˆ₯π–Ώπ—‚π–»π—π—ˆπ—π–Ίπ—…β’(f)((x,v))βˆ₯n is contractible if and only if βˆ₯𝖿𝗂𝖻f⁒(x)⁒(v)βˆ₯n is contractible. ∎

Another useful fact about connected maps is that they induce an equivalence on n-truncations:

Lemma 7.5.14.

If f:Aβ†’B is n-connected, then it induces an equivalence βˆ₯Aβˆ₯n≃βˆ₯Bβˆ₯n.


Let c be the proof that f is n-connected. From left to right, we use the map βˆ₯fβˆ₯n:βˆ₯Aβˆ₯nβ†’βˆ₯Bβˆ₯n. To define the map from right to left, by the universal property of truncations, it suffices to give a map 𝖻𝖺𝖼𝗄:Bβ†’βˆ₯Aβˆ₯n. We can define this map as follows:


By definition, c⁒(y) has type π—‚π—Œπ–’π—ˆπ—‡π—π—‹(βˆ₯𝖿𝗂𝖻f(y)βˆ₯n), so its first component has type βˆ₯𝖿𝗂𝖻f⁒(y)βˆ₯n, and we can obtain an element of βˆ₯Aβˆ₯n from this by projection.

Next, we show that the composites are the identityPlanetmathPlanetmathPlanetmath. In both directions, because the goal is a path in an n-truncated type, it suffices to cover the case of the constructor |–|n.

In one direction, we must show that for all x:A,


But |(x,𝗋𝖾𝖿𝗅)|n:βˆ₯𝖿𝗂𝖻f(y)βˆ₯n, and c⁒(y) says that this type is contractible, so


Applying βˆ₯𝗉𝗋1βˆ₯n to both sides of this equation gives the result.

In the other direction, we must show that for all y:B,


𝗉𝗋1⁒(c⁒(y)) has type βˆ₯𝖿𝗂𝖻f⁒(y)βˆ₯n, and the path we want is essentially the second component of the 𝖿𝗂𝖻f⁒(y), but we need to make sure the truncations work out.

In general, suppose we are given p:βˆ₯βˆ‘(x:A)B(x)βˆ₯n and wish to prove P(βˆ₯𝗉𝗋1βˆ₯n(p)). By truncation induction, it suffices to prove P(|a|n) for all a:A and b:B⁒(a). Applying this principle in this case, it suffices to prove


given a:A and b:f⁒(a)=y. But the left-hand side equals |f⁒(a)|n, so applying |–|n to both sides of b gives the result. ∎

One might guess that this fact characterizes the n-connected maps, but in fact being n-connected is a bit stronger than this. For instance, the inclusion 0𝟐:πŸβ†’πŸ induces an equivalence on (-1)-truncations, but is not surjective (i.e.Β (-1)-connected). In Β§8.4 (http://planetmath.org/84fibersequencesandthelongexactsequence) we will see that the differencePlanetmathPlanetmath in general is an analogous extra bit of surjectivity.

Title 7.5 Connectedness