In §3.7 (http://planetmath.org/37propositionaltruncation) we introduced the propositional truncation, which makes the “best approximation” of a type that is a mere proposition, i.e. a -type. In §6.9 (http://planetmath.org/69truncations) we constructed this truncation as a higher inductive type, and gave one way to generalize it to a 0-truncation. We now explain a better generalization of this, which truncates any type into an -type for any ; in classical homotopy theory this would be called its Postnikov section.
The idea is to make use of (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), which states that is an -type just when is contractible for all , and Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3), which implies that where is equipped with some basepoint which we may as well call . However, contractibility of is something that we can ensure directly by giving path constructors.
We might first of all try to define to be generated by a function , together with for each and each , a path . But this does not quite work, for the same reason that Remark 6.7.1 (http://planetmath.org/67hubsandspokes#Thmprermk1) fails. Instead, we use the full “hub and spoke” construction as in §6.7 (http://planetmath.org/67hubsandspokes).
Thus, for , we take to be the higher inductive type generated by:
a function ,
for each , a hub point , and
for each and each , a spoke path .
The existence of these constructors is now enough to show:
is an -type.
By (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), it suffices to show that is contractible for all , which by Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3) is equivalent to As center of contraction for the latter, we choose the function which is constant at , together with .
Now, an arbitrary element of consists of a map together with a path . By function extensionality, to show it suffices to give, for each , a path . We choose this to be the composite , where is the spoke at .
(This construction fails for , but in that case we can simply define for all . From now on we assume .)
For each , an element ,
For each and , an element ,
For each and , and each , a dependent path ,
there exists a section with for all . To make this more useful, we reformulate it as follows.
For any type family such that each is an -type, and any function , there exists a section such that for all .
It will suffice to construct the second and third data listed above, since has exactly the type of the first datum. Given and , we have and . Define by . Then since is -truncated, there exists a point and a contraction . Define , giving the second datum. Then (recalling the definition of dependent paths), has exactly the type required of the third datum. ∎
In particular, if is some -type, we can consider the constant family of types equal to for every point of . Thus, every map can be extended to a map defined by ; this is the recursion principle for .
The induction principle also implies a uniqueness principle for functions of this form. Namely, if is an -type and are such that for every , then for all , since the type is an -type. Thus, . This yields the following universal property.
Lemma 7.3.3 (Universal property of truncations).
Let , and . The following map is an equivalence:
Given that is -truncated, any can be extended to a map . The map is equal to , because for every we have by definition. And the map is equal to , because they both send to . ∎
In categorical language, this says that the -types form a reflective subcategory of the category of types. (To state this fully precisely, one ought to use the language of -categories.) In particular, this implies that the -truncation is functorial: given , applying the recursion principle to the composite yields a map . By definition, we have a homotopy
expressing naturality of the maps .
Uniqueness implies functoriality laws such as and , with attendant coherence laws. We also have higher functoriality, for instance:
Given and a homotopy , there is an induced homotopy such that the composite
is equal to .
First, we indeed have a homotopy with components . Composing on either sides with the paths and , which arise from the definitions of and , we obtain a homotopy , and hence an equality by function extensionality. But since is an equivalence, there must be a path inducing it, and the coherence laws for function extensionality imply (7.3.5). ∎
The following observation about reflective subcategories is also standard.
A type is an -type if and only if is an equivalence.
“If” follows from closure of -types under equivalence. On the other hand, if is an -type, we can define . Then we have by definition. In order to prove that , we only need to prove that . This is again true:
The category of -types also has some special properties not possessed by all reflective subcategories. For instance, the reflector preserves finite products.
For any types and , the induced map is an equivalence.
It suffices to show that has the same universal property as . Thus, let be an -type; we have
using the universal properties of and , along with the fact that is an -type since is. It is straightforward to verify that this equivalence is given by composing with , as needed. ∎
The following related fact about dependent sums is often useful.
Let be a family of types. Then there is an equivalence
We use the induction principle of -truncation several times to construct functions
and homotopies and exhibiting them as quasi-inverses. We define by setting . We define by setting . Then we define and . ∎
If is an -type and is any type family, then
If is an -type, then the left-hand type above is already an -type, hence equivalent to its -truncation; thus this follows from Theorem 7.3.9 (http://planetmath.org/73truncations#Thmprethm3). ∎
We can characterize the path spaces of a truncation using the same method that we used in §2.12 (http://planetmath.org/212coproducts),§2.13 (http://planetmath.org/213naturalnumbers) for coproducts and natural numbers (and which we will use in http://planetmath.org/node/87582Chapter 8 to calculate homotopy groups). Unsurprisingly, the path spaces in the -truncation of are the -truncations of the path spaces of . Indeed, for any there is a canonical map
This definition uses the recursion principle for , which is correct because is -truncated, so that the codomain of is -truncated.
For any and and , the map (7.3.11) is an equivalence; thus we have
The proof is a simple application of the encode-decode method: As in previous situations, we cannot directly define a quasi-inverse to the map (7.3.11) because there is no way to induct on an equality between and . Thus, instead we generalize its type, in order to have general elements of the type instead of and . Define by
This definition is correct because is -truncated, and is -truncated by Theorem 7.1.11 (http://planetmath.org/71definitionofntypes#Thmprethm7). Now for every , there is a map
defined for and and by
Since the codomain of is -truncated, it suffices to define it only for and of this form, and then it’s just the same definition as before. We also define a function
by induction on , where .
Now we can define an inverse map
To show that the composite
is the identity function, by path induction it suffices to check it for , in which case what we need to know is that . But since this is an -type, hence also an -type, we may assume , in which case it follows by definition of and . Finally, to show that
is the identity function, since this goal is again an -type, we may assume that and and that we are considering for some . Then we have
This completes the proof that and are quasi-inverses. The stated result is then the special case where and . ∎
Let and be a pointed type. Then
This is a special case of the previous lemma where . ∎
Let and and a pointed type. Then
By induction on , using the recursive definition of . ∎
We also observe that “truncations are cumulative”: if we truncate to an -type and then to a -type with , then we might as well have truncated directly to a -type.
Let with and . Then .
We define two maps and by
The map is well-defined because is -truncated and also -truncated (because ), and the map is well-defined because is -truncated.
The composition satisfies , hence . Similarly, we have and hence . ∎