Cellular Methods in Homotopy Type Theory

In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Thanks to their excellent categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject -perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes.

In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result, which we call the "Hurewicz approximation theorem", shows that the CW complexes that are n-connected types are precisely the ones that can be presented by a CW structure with no nontrivial cells up to dimension n. This theorem is standard in the classical treatment of CW complexes, but it is far from being obvious in a constructive setting. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.