6.7 Hubs and spokes

In topology, one usually speaks of building CW complexes by attaching $n$-dimensional discs along their $(n-1)$-dimensional boundary spheres.However, another way to express this is by gluing in the cone on an $(n-1)$-dimensional sphere.That is, we regard a disc as consisting of a cone point (or “hub”), with meridians(or “spokes”) connecting that point to every point on the boundary, continuously, as shown in Figure 6.3 (http://planetmath.org/67hubsandspokes#S0.F3).

HoTT_fig_6.7.1.png

Figure 6.3: A 2-disc made out of a hub and spokes

We can use this idea to express higher inductive types containing $n$-dimensional path-constructors for $n>1$ in terms of ones containing only 1-dimensional path-constructors.The point is that we can obtain an $n$-dimensional path as a continuous family of 1-dimensional paths parametrized by an $(n-1)$-dimensional object.The simplest $(n-1)$-dimensional object to use is the $(n-1)$-sphere, although in some cases a different one may be preferable.(Recall that we were able to define the spheres in §6.5 (http://planetmath.org/65suspensions) inductively using suspensions, which involve only 1-dimensional path constructors.Indeed, suspension can also be regarded as an instance of this idea, since it involves a family of 1-dimensional paths parametrized by the type being suspended.)

For instance, the torus $T^2$ from the previous section could be defined instead to be generated by:

• a point $b:T^2$,

• a path $p:b=b$,

• another path $q:b=b$,

• a point $h:T^2$, and

• for each $x:{𝕊}^1$, a path $s(x):f(x)=h$, where $f:{𝕊}^1\to T^2$ is defined by $f(\mathrm{𝖻𝖺𝗌𝖾}):\equiv b$ and $f\left(\mathrm{𝗅𝗈𝗈𝗉}\right):=pq{p}^{-1}{q}^{-1}$.

The induction principle for this version of the torus says that 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 }$,

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

• for each $x:{𝕊}^1$, a path $g(x){=}_{s(x)}^P{h}^{\prime }$, where $g:{\prod }_{(x:{𝕊}^1)}P(f(x))$ is defined by $g(\mathrm{𝖻𝖺𝗌𝖾}):\equiv b^{\prime }$ and ${\mathrm{𝖺𝗉𝖽}}_g\left(\mathrm{𝗅𝗈𝗈𝗉}\right):=p^{\prime }{q}^{\prime }{(p^{\prime })}^{-1}{(q^{\prime })}^{-1}$.

Note that there is no need for dependent 2-paths or ${\mathrm{𝖺𝗉𝖽}}^2$.We leave it to the reader to write out the computation rules.

Remark 6.7.1.

One might question the need for introducing the hub point $h$; why couldn’t we instead simply add paths continuously relating the boundary of the disc to a point on that boundary, as shown in Figure 6.4 (http://planetmath.org/67hubsandspokes#S0.F5)?This does work, but not as well.For if, given some $f\mathrm{:}{\mathrm{S}}^{\mathrm{1}}\mathrm{\to }X$, we give a path constructor connecting each $f\mathit{}\mathrm{(}x\mathrm{)}$ to $f\mathit{}\mathrm{(}\mathrm{base}\mathrm{)}$, then what we end up with is more like the picture in Figure 6.5 (http://planetmath.org/67hubsandspokes#S0.F5) of a cone whose vertex is twisted around and glued to some point on its base.The problem is that the specified path from $f\mathit{}\mathrm{(}\mathrm{base}\mathrm{)}$ to itself may not be reflexivity.We could add a 2-dimensional path constructor ensuring this, but using a separate hub avoids the need for any path constructors of dimension above $\mathrm{1}$.

HoTT_fig_6.7.2a.png

Figure 6.4: Hubless spokes

HoTT_fig_6.7.2b.png

Figure 6.5: Hubless spokes, II

Remark 6.7.2.

Note also that this “translation” of higher paths into 1-paths does not preserve judgmental computation rules for these paths, though it does preserve propositional ones.