Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

kangrongji
Copy link
Contributor

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
Copy link
Contributor Author

kangrongji commented Sep 19, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant