6.7 Hubs and spokes

In topologyMathworldPlanetmath, 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).



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 continuousMathworldPlanetmathPlanetmath 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 suspensionsMathworldPlanetmath, 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 T2 from the previous sectionPlanetmathPlanetmathPlanetmathPlanetmath could be defined instead to be generated by:

  • a point b:T2,

  • a path p:b=b,

  • another path q:b=b,

  • a point h:T2, and

  • for each x:𝕊1, a path s(x):f(x)=h, where f:𝕊1T2 is defined by f(𝖻𝖺𝗌𝖾):b and f(𝗅𝗈𝗈𝗉):=p\centerdotq\centerdotp-1\centerdotq-1.

The inductionMathworldPlanetmath principle for this version of the torus says that given P:T2𝒰, for a section (x:T2)P(x) we require

  • a point b:P(b),

  • a path p:b=pPb,

  • a path q:b=qPb,

  • a point h:P(h), and

  • for each x:𝕊1, a path g(x)=s(x)Ph, where g:(x:𝕊1)P(f(x)) is defined by g(𝖻𝖺𝗌𝖾):b and 𝖺𝗉𝖽g(𝗅𝗈𝗈𝗉):=p\centerdotq\centerdot(p)-1\centerdot(q)-1.

Note that there is no need for dependent 2-paths or 𝖺𝗉𝖽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:S1X, we give a path constructor connecting each f(x) to f(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(base) to itself may not be reflexivityMathworldPlanetmath. We could add a 2-dimensional path constructor ensuring this, but using a separate hub avoids the need for any path constructors of dimensionMathworldPlanetmath above 1.



Figure 6.4: Hubless spokes


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