6.9 Truncations

In Β§3.7 (http://planetmath.org/37propositionaltruncation) we introduced the propositional truncation as a new type forming operationMathworldPlanetmath; we now observe that it can be obtained as a special case of higher inductive types. This reduces the problem of understanding truncations to the problem of understanding higher inductives, which at least are amenable to a systematic treatment. It is also interesting because it provides our first example of a higher inductive type which is truly recursive, in that its constructors take inputs from the type being defined (as does the successorMathworldPlanetmathPlanetmathPlanetmath π—Œπ—Žπ–Όπ–Ό:β„•β†’β„•).

Let A be a type; we define its propositional truncation βˆ₯Aβˆ₯ to be the higher inductive type generated by:

  • β€’

    A function |–|:Aβ†’βˆ₯Aβˆ₯, and

  • β€’

    For each x,y:βˆ₯Aβˆ₯, a path x=y.

Note that the second constructor is by definition the assertion that βˆ₯Aβˆ₯ is a mere proposition. Thus, the definition of βˆ₯Aβˆ₯ can be interpreted as saying that βˆ₯Aβˆ₯ is freely generated by a function Aβ†’βˆ₯Aβˆ₯ and the fact that it is a mere proposition.

The recursion principle for this higher inductive definition is easy to write down: it says that given any type B together with

  • β€’

    A function g:A→B, and

  • β€’

    For any x,y:B, a path x=By,

there exists a function f:βˆ₯Aβˆ₯β†’B such that

  • β€’

    f(|a|)≑g(a) for all a:A, and

  • β€’

    for any x,y:βˆ₯Aβˆ₯, the function 𝖺𝗉f takes the specified path x=y in βˆ₯Aβˆ₯ to the specified path f⁒(x)=f⁒(y) in B (propositionally).

These are exactly the hypotheses that we stated in Β§3.7 (http://planetmath.org/37propositionaltruncation) for the recursion principle of propositional truncation β€” a function Aβ†’B such that B is a mere proposition β€” and the first part of the conclusionMathworldPlanetmath is exactly what we stated there as well. The second part (the action of 𝖺𝗉f) was not mentioned previously, but it turns out to be vacuousPlanetmathPlanetmath in this case, because B is a mere proposition, so any two paths in it are automatically equal.

There is also an inductionMathworldPlanetmath principle for βˆ₯Aβˆ₯, which says that given any B:βˆ₯Aβˆ₯→𝒰 together with

  • β€’

    a function g:∏(a:A)B(|a|), and

  • β€’

    for any x,y:βˆ₯Aβˆ₯ and u:B⁒(x) and v:B⁒(y), a dependent path q:u=p⁒(x,y)Bv, where p⁒(x,y) is the path coming from the second constructor of βˆ₯Aβˆ₯,

there exists f:∏(x:βˆ₯Aβˆ₯)B⁒(x) such that f(|a|)≑a for a:A, and also another computation rule. However, because there can be at most one function between any two mere propositions (up to homotopy), this induction principle is not really useful (see also http://planetmath.org/node/87806Exercise 3.20).

We can, however, extend this idea to construct similar truncations landing in n-types, for any n. For instance, we might define the 0-truncation βˆ₯Aβˆ₯0 to be generated by

  • β€’

    A function |–|0:Aβ†’βˆ₯Aβˆ₯0, and

  • β€’

    For each x,y:βˆ₯Aβˆ₯0 and each p,q:x=y, a path p=q.

Then βˆ₯Aβˆ₯0 would be freely generated by a function Aβ†’βˆ₯Aβˆ₯0 together with the assertion that βˆ₯Aβˆ₯0 is a set. A natural induction principle for it would say that given B:βˆ₯Aβˆ₯0→𝒰 together with

  • β€’

    a function g:∏(a:A)B(|a|0), and

  • β€’

    for any x,y:βˆ₯Aβˆ₯0 with z:B⁒(x) and w:B⁒(y), and each p,q:x=y with r:z=pBw and s:z=qBw, a 2-path v:p=u⁒(x,y,p,q)Bq, where u⁒(x,y,p,q):p=q is obtained from the second constructor of βˆ₯Aβˆ₯0,

there exists f:∏(x:βˆ₯Aβˆ₯0)B⁒(x) such that f(|a|0)≑g(a) for all a:A, and also 𝖺𝗉𝖽f2(u(x,y,p,q)) is the 2-path specified above. (As in the propositional case, the latter condition turns out to be uninteresting.) From this, however, we can prove a more useful induction principle.

Lemma 6.9.1.

Suppose given B:βˆ₯Aβˆ₯0β†’U together with g:∏(a:A)B(|a|0), and assume that each B⁒(x) is a set. Then there exists f:∏(x:βˆ₯Aβˆ₯0)B⁒(x) such that f(|a|0)≑g(a) for all a:A.


It suffices to construct, for any x,y,z,w,p,q,r,s as above, a 2-path v:p=u⁒(x,y,p,q)Bq. However, by the definition of dependent 2-paths, this is an ordinary 2-path in the fiber B⁒(y). Since B⁒(y) is a set, a 2-path exists between any two parallel paths. ∎

This implies the expected universal property.

Lemma 6.9.2.

For any set B and any type A, composition with |–|0:Aβ†’βˆ₯Aβˆ₯0 determines an equivalence


The special case of Lemma 6.9.1 (http://planetmath.org/69truncations#Thmprelem1) when B is the constant family gives a map from right to left, which is a right inverseMathworldPlanetmath to the β€œcompose with |–|0” function from left to right. To show that it is also a left inverse, let h:βˆ₯Aβˆ₯0β†’B, and define hβ€²:βˆ₯Aβˆ₯0β†’B by applying Lemma 6.9.1 (http://planetmath.org/69truncations#Thmprelem1) to the composite a↦h(|a|0). Thus, hβ€²(|a|0)=h(|a|0).

However, since B is a set, for any x:βˆ₯Aβˆ₯0 the type h⁒(x)=h′⁒(x) is a mere proposition, and hence also a set. Therefore, by Lemma 6.9.1 (http://planetmath.org/69truncations#Thmprelem1), the observation that hβ€²(|a|0)=h(|a|0) for any a:A implies h⁒(x)=h′⁒(x) for any x:βˆ₯Aβˆ₯0, and hence h=hβ€². ∎

For instance, this enables us to construct colimits of sets. We have seen that if A←𝑓C→𝑔B is a span of sets, then the pushout AβŠ”CB may no longer be a set. (For instance, if A and B are 𝟏 and C is 𝟐, then the pushout is π•Š1.) However, we can construct a pushout that is a set, and has the expected universal property with respect to other sets, by truncating.

Lemma 6.9.3.

Let A←𝑓C→𝑔B be a span of sets. Then for any set E, there is a canonical equivalence


Compose the equivalences in Lemma 6.8.2 (http://planetmath.org/68pushouts#Thmprelem1),Lemma 6.9.2 (http://planetmath.org/69truncations#Thmprelem2). ∎

We refer to βˆ₯AβŠ”CBβˆ₯0 as the set-pushout of f and g, to distinguish it from the (homotopy) pushout AβŠ”CB. Alternatively, we could modify the definition of the pushout in Β§6.8 (http://planetmath.org/68pushouts) to include the 0-truncation constructor directly, avoiding the need to truncate afterwards. Similar remarks apply to any sort of colimit of sets; we will explore this further in http://planetmath.org/node/87584Chapter 10.

However, while the above definition of the 0-truncation works β€” it gives what we want, and is consistent β€” it has a couple of issues. Firstly, it doesn’t fit so nicely into the general theory of higher inductive types. In general, it is tricky to deal directly with constructors such as the second one we have given for βˆ₯Aβˆ₯0, whose inputs involve not only elements of the type being defined, but paths in it.

This can be gotten round fairly easily, however. Recall in Β§5.1 (http://planetmath.org/51introductiontoinductivetypes) we mentioned that we can allow a constructor of an inductive type W to take β€œinfinitely many argumentsMathworldPlanetmath” of type W by having it take a single argument of type β„•β†’W. There is a general principle behind this: to model a constructor with funny-looking inputs, use an auxiliary inductive type (such as β„•) to parametrize them, reducing the input to a simple functionMathworldPlanetmathPlanetmath with inductive domain.

For the 0-truncation, we can consider the auxiliary higher inductive type S generated by two points a,b:S and two paths p,q:a=b. Then the fishy-looking constructor of βˆ₯Aβˆ₯0 can be replaced by the unobjectionable

  • β€’

    For every f:Sβ†’A, a path 𝖺𝗉f⁒(p)=𝖺𝗉f⁒(q).

Since to give a map out of S is the same as to give two points and two parallel paths between them, this yields the same induction principle.

A more serious problem with our current definition of 0-truncation, however, is that it doesn’t generalize very well. If we want to describe a notion of definition of β€œn-truncation” into n-types uniformly for all n:β„•, then this approach is unfeasible, since the second constructor would need a number of arguments that increases with n. In Β§7.3 (http://planetmath.org/73truncations), therefore, we will use a different idea to construct these, based on the observation that the type S introduced above is equivalentMathworldPlanetmathPlanetmathPlanetmath to the circle π•Š1. This includes the 0-truncation as a special case, and satisfies generalized versions of Lemma 6.9.1 (http://planetmath.org/69truncations#Thmprelem1),Lemma 6.9.2 (http://planetmath.org/69truncations#Thmprelem2).

Title 6.9 Truncations