6.7 Hubs and spokes
In topology^{}, one usually speaks of building CW complexes by attaching $n$dimensional discs along their $(n1)$dimensional boundary spheres. However, another way to express this is by gluing in the cone on an $(n1)$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 pathconstructors for $n>1$ in terms of ones containing only 1dimensional pathconstructors. The point is that we can obtain an $n$dimensional path as a continuous^{} family of 1dimensional paths parametrized by an $(n1)$dimensional object. The simplest $(n1)$dimensional object to use is the $(n1)$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 1dimensional path constructors. Indeed, suspension can also be regarded as an instance of this idea, since it involves a family of 1dimensional 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(\mathrm{\U0001d5bb\U0001d5ba\U0001d5cc\U0001d5be}):\equiv b$ and $f\left(\mathrm{\U0001d5c5\U0001d5c8\U0001d5c8\U0001d5c9}\right):=p\text{centerdot}q\text{centerdot}{p}^{1}\text{centerdot}{q}^{1}$.
The induction^{} principle for this version of the torus says that given $P:{T}^{2}\to \mathcal{U}$, 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:{\mathbb{S}}^{1}$, a path $g(x){=}_{s(x)}^{P}{h}^{\prime}$, where $g:{\prod}_{(x:{\mathbb{S}}^{1})}P(f(x))$ is defined by $g(\mathrm{\U0001d5bb\U0001d5ba\U0001d5cc\U0001d5be}):\equiv {b}^{\prime}$ and ${\mathrm{\U0001d5ba\U0001d5c9\U0001d5bd}}_{g}\left(\mathrm{\U0001d5c5\U0001d5c8\U0001d5c8\U0001d5c9}\right):={p}^{\prime}\text{centerdot}{q}^{\prime}\text{centerdot}{({p}^{\prime})}^{1}\text{centerdot}{({q}^{\prime})}^{1}$.
Note that there is no need for dependent 2paths or ${\mathrm{\U0001d5ba\U0001d5c9\U0001d5bd}}^{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 2dimensional path constructor ensuring this, but using a separate hub avoids the need for any path constructors of dimension^{} above $\mathrm{1}$.
Remark 6.7.2.
Note also that this “translation” of higher paths into 1paths does not preserve judgmental computation rules for these paths, though it does preserve propositional ones.
Title  6.7 Hubs and spokes 

\metatable 