7. Homotopy n-types

One of the basic notions of homotopy theory is that of a homotopy $n$-type: a space containing no interesting homotopy above dimension $n$. For instance, a homotopy $0$-type is essentially a set, containing no nontrivial paths, while a homotopy $1$-type may contain nontrivial paths, but no nontrivial paths between paths. Homotopy $n$-types are also called $n$-truncated spaces. We have mentioned this notion already in §3.1 (http://planetmath.org/31setsandntypes); our first goal in this chapter is to give it a precise definition in homotopy type theory.

A dual notion to truncatedness is connectedness: a space is $n$-connected if it has no interesting homotopy in dimensions $n$ and below. For instance, a space is $0$-connected (also called just “connected”) if it has only one connected component, and $1$-connected (also called “simply connected”) if it also has no nontrivial loops (though it may have nontrivial higher loops between loops).

The duality between truncatedness and connectedness is most easily seen by extending both notions to maps. We call a map $n$-truncated or $n$-connected if all its fibers are so. Then $n$-connected and $n$-truncated maps form the two classes of maps in an orthogonal factorization system, i.e. every map factors uniquely as an $n$-connected map followed by an $n$-truncated one.

In the case $n=-1$, the $n$-truncated maps are the embeddings and the $n$-connected maps are the surjections, as defined in §4.6 (http://planetmath.org/46surjectionsandembeddings). Thus, the $n$-connected factorization system is a massive generalization of the standard image factorization of a function between sets into a surjection followed by an injection. At the end of this chapter, we sketch briefly an even more general theory: any type-theoretic modality gives rise to an analogous factorization system.

Title	7. Homotopy n-types