search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

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

Open kangrongji opened 11 months ago

kangrongji commented 11 months ago

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 commented 11 months ago

@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.