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).

\includegraphics

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:\mathbb{S}^{1}$ , a path $s(x):f(x)=h$ , where $f:\mathbb{S}^{1}\to T^{2}$ is defined by $f(\mathsf{base}):\!\!\equiv b$ and ${f}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}:=p\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{p% }^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{q}^{-1}}$ .

The induction principle for this version of the torus says that given $P:T^{2}\to\mathcal{U}$ , for a section $\mathchoice{\prod_{x:T^{2}}\,}{\mathchoice{{\textstyle\prod_{(x:T^{2})}}}{% \prod_{(x:T^{2})}}{\prod_{(x:T^{2})}}{\prod_{(x:T^{2})}}}{\mathchoice{{% \textstyle\prod_{(x:T^{2})}}}{\prod_{(x:T^{2})}}{\prod_{(x:T^{2})}}{\prod_{(x:% T^{2})}}}{\mathchoice{{\textstyle\prod_{(x:T^{2})}}}{\prod_{(x:T^{2})}}{\prod_% {(x:T^{2})}}{\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}=^{P}_{q}b^{\prime}$ ,
•

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

for each $x:\mathbb{S}^{1}$ , a path $g(x)=^{P}_{s(x)}h^{\prime}$ , where $g:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}P(f(% x))$ is defined by $g(\mathsf{base}):\!\!\equiv b^{\prime}$ and $\mathsf{apd}_{g}\mathopen{}\left(\mathsf{loop}\right)\mathclose{}:=p^{\prime}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q^{\prime}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}% }}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{(p^{\prime})}^{-1}}\mathchoice{\mathbin{\raisebox{% 2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}% }{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{(q^{\prime})}% ^{-1}}$ .

Note that there is no need for dependent 2-paths or $\mathsf{apd}^{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:\mathbb{S}^{1}\to X$ , we give a path constructor connecting each $f(x)$ to $f(\mathsf{base})$ , 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(\mathsf{base})$ 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 $1$ .

\includegraphics

HoTT_fig_6.7.2a.png

Figure 6.4: Hubless spokes

\includegraphics

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.

Title	6.7 Hubs and spokes
\metatable