6.6 Cell complexes

In classical topology, a cell complex is a space obtained by successively attaching discs along their boundaries.It is called a CW complex if the boundary of an $n$-dimensional disc is constrained to lie in the discs of dimension strictly less than $n$ (the $(n-1)$-skeleton).

Any finite CW complex can be presented as a higher inductive type, by turning $n$-dimensional discs into $n$-dimensional paths and partitioning the image of the attaching map into a source and a target, with each written as a composite of lower dimensional paths.Our explicit definitions of ${𝕊}^1$ and ${𝕊}^2$ in §6.4 (http://planetmath.org/64circlesandspheres) had this form.

Another example is the torus $T^2$, which is generated by:

• a point $b:T^2$,

• a path $p:b=b$,

• another path $q:b=b$, and

• a 2-path $t:pq=qp$.

Perhaps the easiest way to see that this is a torus is to start with a rectangle, having four corners $a,b,c,d$, four edges $p,q,r,s$, and an interior which is manifestly a 2-path $t$ from $pq$ to $rs$:

HoTT_fig_6.6.1.png

Now identify the edge $r$ with $q$ and the edge $s$ with $p$, resulting in also identifying all four corners.Topologically, this identification can be seen to produce a torus.

The induction principle for the torus is the trickiest of any we’ve written out so far.Given $P:T^2\to 𝒰$, for a section ${\prod }_{(x:T^2)}P(x)$ we require

• a point $b^{\prime }:P(b)$,

• a path $p^{\prime }:b^{\prime }{=}_p^P{b}^{\prime }$,

• a path $q^{\prime }:b^{\prime }{=}_q^P{b}^{\prime }$, and

• a 2-path $t^{\prime }$ between the “composites” $p^{\prime }{q}^{\prime }$ and $q^{\prime }{p}^{\prime }$, lying over $t$.

In order to make sense of this last datum, we need a composition operation for dependent paths, but this is not hard to define.Then the induction principle gives a function $f:{\prod }_{(x:T^2)}P(x)$ such that $f(b)\equiv b^{\prime }$ and ${\mathrm{𝖺𝗉𝖽}}_f\left(p\right)=p^{\prime }$ and ${\mathrm{𝖺𝗉𝖽}}_f\left(q\right)=q^{\prime }$ and something like “${\mathrm{𝖺𝗉𝖽}}_f^2\left(t\right)=t^{\prime }$”.However, this is not well-typed as it stands, firstly because the equalities ${\mathrm{𝖺𝗉𝖽}}_f\left(p\right)=p^{\prime }$ and ${\mathrm{𝖺𝗉𝖽}}_f\left(q\right)=q^{\prime }$ are not judgmental, and secondly because ${\mathrm{𝖺𝗉𝖽}}_f$ only preserves path concatenation up to homotopy.We leave the details to the reader (see http://planetmath.org/node/87797Exercise 6.1).

Of course, another definition of the torus is $T^2:\equiv {𝕊}^1\times {𝕊}^1$ (in http://planetmath.org/node/87800Exercise 6.3 we ask the reader to verify the equivalence of the two).The cell-complex definition, however, generalizes easily to other spaces without such descriptions, such as the Klein bottle, the projective plane, etc.But it does get increasingly difficult to write down the induction principles, requiring us to define notions of dependent $n$-paths and of $\mathrm{𝖺𝗉𝖽}$ acting on $n$-paths.Fortunately, once we have the spheres in hand, there is a way around this.