Higher-dimensional paths as parametrizations of 1-dimensional paths

Question

Sect. 6.7 of the HoTT Book establishes in the context of CW complexes that

"we can obtain an n-dimensional path as a continuous family of 1-dimensional paths parametrized by an (n − 1)-dimensional object"

I hope I'm correct in taking this to be also the basic principle that allows to construct $S^n$ as iterated homotopy pushouts.

In analogy with "plain" geometric dimensions, we can maybe think of this as follows: The 2-dimensional plane can be described by a 1-dimensional line parametrized by another 1-dimensional line: For each x-coordinate, I'll give you a line of y-coordinates. This also brings to mind the idea of currying.

So it seems like a very fundamental fact that we can construct higher-dimensional objects by plugging lower-dimensional objects into each other, and I'm as a more syntactically minded type theorist would like to understand this better. Are there basic references in algebraic topology which provide an explanation of this?

Also, I presume this has been used utilized in the construction of higher-dimensional type theories, for instance, Cubical Agda defines the 3-dimensional path for the $S^3$ as some nested PathPs:

surf : PathP (λ j → PathP (λ i → base ≡ base) refl refl) refl refl

Does Cubical Agda get by with only 1-dimensional paths, or is there internally a direct representation of higher-dimensional paths?

Answer 1

I'm not quite sure what you're asking for with the first question, but have you looked at some basic algebraic topology books that work with CW-complexes, e.g. Hatcher? For instance, I believe Hatcher discusses the topological fact that the product of two CW-complexes $X$ and $Y$ is a CW-complex whose cells are products of a cell in $X$ and a cell in $Y$, where the product of an $m$-dimensional cell and an $n$-dimensional cell is $(m+n)$-dimensional. (Unfortunately in the topological case the discussion of this is somewhat muddied by point-set-topological technicalities, e.g. Hatcher's Theorem A.6, but the intuition is there.) There are also algebraic manifestations of this "dimension-adding" property, e.g. the tensor product of chain complexes or graded modules, which corresponds closely via the Kunneth theorem to products of spaces.

Regarding the second question, I don't believe that cubical Agda has a basic type-forming operation that represents higher-dimensional paths, although it would be consistent to add such a thing, e.g. using the idea of general "extension types" introduced in A type theory for synthetic ∞-categories. However, like all cubical type theories, cubical Agda does have a judgmental representation of higher-dimensional "paths", namely a term whose context contains multiple dimension variables. Of course, one could say that this is still representing them in terms of 1-dimensional paths, by currying, i.e. a 2-dimensional path (square) is a path parametrized by a path -- which is, again, the same observation you started with.