The General Extend Operation (a.k.a. The Cube-Filling Macro)

[kangrongji]

This PR implements the general version of extendₙ for all values of n. It's a fortunate development that this operation be done in the current version of Cubical Agda. Only a small macro is needed to transform external natural numbers to internal ones. It also completes the long-overdue cube-filling macro project. The old PR #910 could be closed now. But I'm not sure about all the old stuff, maybe they'll have some use by someone else... @mortberg

[kangrongji]

@ecavallo Does this construction use any discouraged features of the interval? I find it hard without "the product of I", and I use an inductive type to achieve it.