Closed kangrongji closed 11 months ago
Added an example at the end of the file. The main application I came up with is the same as in #910. I believe this new approach is better. It's simpler and the inductive pattern is very clear. However, I'm unsure if Agda's meta-programming could handle partial elements and (non-fibrant) extension types that needed.
But since these operations are more general than just cube-filling (they allow for an arbitrary cofibration ϕ
), I think they could have other uses. Perhaps it can help with some arguments involving n-types... Sadly I don't have a specific example in mind at this moment.
Btw, I also think the cube-filling results in library need reorganization. They are separated in several files like here, here and here. Maybe they would be better put together and deduced as consequences of these extend
operations.
Added an example at the end of the file. The main application I came up with is the same as in #910. I believe this new approach is better. It's simpler and the inductive pattern is very clear. However, I'm unsure if Agda's meta-programming could handle partial elements and (non-fibrant) extension types that needed.
But since these operations are more general than just cube-filling (they allow for an arbitrary cofibration
ϕ
), I think they could have other uses. Perhaps it can help with some arguments involving n-types... Sadly I don't have a specific example in mind at this moment.Btw, I also think the cube-filling results in library need reorganization. They are separated in several files like here, here and here. Maybe they would be better put together and deduced as consequences of these
extend
operations.
Yeah, reorganizing them a bit sounds very reasonable. Feel free to do it in a future PR!
I'm happy with this one now so will merge
I haven't worked on the cube-filling stuff in quite some time. However, I recently discovered a surprisingly easy way to do the same job with just a few lines of code. In fact the result seems to be more powerful than the previous one. I've written a short note about this, which you can find here.
I'm curious whether or not someone in the cubical type theory community has found this before, since it is so simple...