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

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

###### 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