6.9 Truncations

In §3.7 (http://planetmath.org/37propositionaltruncation) we introduced the propositional truncation as a new type forming operation; 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 successor $\mathsf{succ}:\mathbb{N}\to\mathbb{N}$ ).

Let $A$ be a type; we define its propositional truncation $\mathopen{}\left\|A\right\|\mathclose{}$ to be the higher inductive type generated by:

•

A function $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|:A\to\mathopen{}\left\|A\right\|% \mathclose{}$ , and
•

For each $x,y:\mathopen{}\left\|A\right\|\mathclose{}$ , a path $x=y$ .

Note that the second constructor is by definition the assertion that $\mathopen{}\left\|A\right\|\mathclose{}$ is a mere proposition. Thus, the definition of $\mathopen{}\left\|A\right\|\mathclose{}$ can be interpreted as saying that $\mathopen{}\left\|A\right\|\mathclose{}$ is freely generated by a function $A\to\mathopen{}\left\|A\right\|\mathclose{}$ 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\to B$ , and
•

For any $x, y : B$ , a path $x=_{B}y$ ,

there exists a function $f:\mathopen{}\left\|A\right\|\mathclose{}\to B$ such that

•

$f(\mathopen{}\left|a\right|\mathclose{})\equiv g(a)$ for all $a : A$ , and
•

for any $x,y:\mathopen{}\left\|A\right\|\mathclose{}$ , the function $\mathsf{ap}_{f}$ takes the specified path $x=y$ in $\mathopen{}\left\|A\right\|\mathclose{}$ 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\to B$ such that $B$ is a mere proposition — and the first part of the conclusion is exactly what we stated there as well. The second part (the action of $\mathsf{ap}_{f}$ ) was not mentioned previously, but it turns out to be vacuous in this case, because $B$ is a mere proposition, so any two paths in it are automatically equal.

There is also an induction principle for $\mathopen{}\left\|A\right\|\mathclose{}$ , which says that given any $B:\mathopen{}\left\|A\right\|\mathclose{}\to\mathcal{U}$ together with

•

a function $g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(\mathopen{}\left|a\right% |\mathclose{})$ , and
•

for any $x,y:\mathopen{}\left\|A\right\|\mathclose{}$ and $u:B(x)$ and $v:B(y)$ , a dependent path $q:u=^{B}_{p(x,y)}v$ , where $p(x,y)$ is the path coming from the second constructor of $\mathopen{}\left\|A\right\|\mathclose{}$ ,

there exists $f:\mathchoice{\prod_{x:\mathopen{}\left\|A\right\|\mathclose{}}\,}{\mathchoice% {{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|\mathclose{})}}}{\prod_{(x:% \mathopen{}\left\|A\right\|\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right% \|\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|\mathclose{})}}}{% \mathchoice{{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|\mathclose{})}}}{% \prod_{(x:\mathopen{}\left\|A\right\|\mathclose{})}}{\prod_{(x:\mathopen{}% \left\|A\right\|\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|% \mathclose{})}}}{\mathchoice{{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|% \mathclose{})}}}{\prod_{(x:\mathopen{}\left\|A\right\|\mathclose{})}}{\prod_{(% x:\mathopen{}\left\|A\right\|\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A% \right\|\mathclose{})}}}B(x)$ such that $f(\mathopen{}\left|a\right|\mathclose{})\equiv 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 $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ to be generated by

•

A function $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{0}:A\to\mathopen{}\left\|A% \right\|_{0}\mathclose{}$ , and
•

For each $x,y:\mathopen{}\left\|A\right\|_{0}\mathclose{}$ and each $p,q:x=y$ , a path $p=q$ .

Then $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ would be freely generated by a function $A\to\mathopen{}\left\|A\right\|_{0}\mathclose{}$ together with the assertion that $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ is a set. A natural induction principle for it would say that given $B:\mathopen{}\left\|A\right\|_{0}\mathclose{}\to\mathcal{U}$ together with

•

a function $g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(\mathopen{}\left|a\right% |_{0}\mathclose{})$ , and
•

for any $x,y:\mathopen{}\left\|A\right\|_{0}\mathclose{}$ with $z:B(x)$ and $w:B(y)$ , and each $p,q:x=y$ with $r:z=^{B}_{p}w$ and $s:z=^{B}_{q}w$ , a 2-path $v:p=^{B}_{u(x,y,p,q)}q$ , where $u(x,y,p,q):p=q$ is obtained from the second constructor of $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ ,

there exists $f:\mathchoice{\prod_{x:\mathopen{}\left\|A\right\|_{0}\mathclose{}}\,}{% \mathchoice{{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}% }}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}{\prod_{(x:% \mathopen{}\left\|A\right\|_{0}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A% \right\|_{0}\mathclose{})}}}{\mathchoice{{\textstyle\prod_{(x:\mathopen{}\left% \|A\right\|_{0}\mathclose{})}}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}{\prod% _{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}}{\mathchoice{{\textstyle% \prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}}{\prod_{(x:\mathopen{% }\left\|A\right\|_{0}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}}B(x)$ such that $f(\mathopen{}\left|a\right|_{0}\mathclose{})\equiv g(a)$ for all $a : A$ , and also $\mathsf{apd}^{2}_{f}\mathopen{}\left(u(x,y,p,q)\right)\mathclose{}$ 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:\mathopen{}\left\|A\right\|_{0}\mathclose{}\to\mathcal{U}$ together with $g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(\mathopen{}\left|a\right% |_{0}\mathclose{})$ , and assume that each $B(x)$ is a set. Then there exists $f:\mathchoice{\prod_{x:\mathopen{}\left\|A\right\|_{0}\mathclose{}}\,}{% \mathchoice{{\textstyle\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}% }}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}{\prod_{(x:% \mathopen{}\left\|A\right\|_{0}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A% \right\|_{0}\mathclose{})}}}{\mathchoice{{\textstyle\prod_{(x:\mathopen{}\left% \|A\right\|_{0}\mathclose{})}}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}{\prod% _{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}}{\mathchoice{{\textstyle% \prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}}{\prod_{(x:\mathopen{% }\left\|A\right\|_{0}\mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}% \mathclose{})}}{\prod_{(x:\mathopen{}\left\|A\right\|_{0}\mathclose{})}}}B(x)$ such that $f(\mathopen{}\left|a\right|_{0}\mathclose{})\equiv g(a)$ for all $a : A$ .

Proof.

It suffices to construct, for any $x, y, z, w, p, q, r, s$ as above, a 2-path $v:p=^{B}_{u(x,y,p,q)}q$ . 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 $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{0}:A\to\mathopen{}\left\|A% \right\|_{0}\mathclose{}$ determines an equivalence

(\mathopen{}\left\|A\right\|_{0}\mathclose{}\to B)\;\simeq\;(A\to B).

Proof.

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 inverse to the “compose with $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{0}$ ” function from left to right. To show that it is also a left inverse, let $h:\mathopen{}\left\|A\right\|_{0}\mathclose{}\to B$ , and define $h^{\prime}:\mathopen{}\left\|A\right\|_{0}\mathclose{}\to B$ by applying Lemma 6.9.1 (http://planetmath.org/69truncations#Thmprelem1) to the composite $a\mapsto h(\mathopen{}\left|a\right|_{0}\mathclose{})$ . Thus, $h^{\prime}(\mathopen{}\left|a\right|_{0}\mathclose{})=h(\mathopen{}\left|a% \right|_{0}\mathclose{})$ .

However, since $B$ is a set, for any $x:\mathopen{}\left\|A\right\|_{0}\mathclose{}$ the type $h(x)=h^{\prime}(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^{\prime}(\mathopen{}\left|a\right|_{0}\mathclose{})=h(\mathopen{}\left|a% \right|_{0}\mathclose{})$ for any $a : A$ implies $h(x)=h^{\prime}(x)$ for any $x:\mathopen{}\left\|A\right\|_{0}\mathclose{}$ , and hence $h=h^{\prime}$ . ∎

For instance, this enables us to construct colimits of sets. We have seen that if $A\xleftarrow{f}C\xrightarrow{g}B$ is a span of sets, then the pushout $A\sqcup^{C}B$ may no longer be a set. (For instance, if $A$ and $B$ are $\mathbf{1}$ and $C$ is $\mathbf{2}$ , then the pushout is $\mathbb{S}^{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\xleftarrow{f}C\xrightarrow{g}B$ be a span of sets. Then for any set $E$ , there is a canonical equivalence

\Bigl{(}\mathopen{}\left\|A\sqcup^{C}B\right\|_{0}\mathclose{}\to E\Bigr{)}\;% \simeq\;\mathsf{cocone}_{\mathscr{D}}(E).

Proof.

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 $\mathopen{}\left\|A\sqcup^{C}B\right\|_{0}\mathclose{}$ as the set-pushout of $f$ and $g$ , to distinguish it from the (homotopy) pushout $A\sqcup^{C}B$ . 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 $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ , 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 arguments” of type $W$ by having it take a single argument of type $\mathbb{N}\to W$ . There is a general principle behind this: to model a constructor with funny-looking inputs, use an auxiliary inductive type (such as $\mathbb{N}$ ) to parametrize them, reducing the input to a simple function 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 $\mathopen{}\left\|A\right\|_{0}\mathclose{}$ can be replaced by the unobjectionable

•

For every $f:S\to A$ , a path $\mathsf{ap}_{f}(p)=\mathsf{ap}_{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:\mathbb{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 equivalent to the circle $\mathbb{S}^{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
\metatable