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?



Higher-dimensional paths as parametrizations of 1-dimensional paths
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](https://pi.math.cornell.edu/%7Ehatcher/AT/AT.pdf)? 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](https://ncatlab.org/nlab/show/tensor+product+of+chain+complexes) or graded modules, which corresponds closely via the [Kunneth theorem](https://ncatlab.org/nlab/show/K%C3%BCnneth+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](https://journals.mq.edu.au/index.php/higher_structures/article/view/36). 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.


