Filling Cubes in a Few Lines of Code #1053
Conversation
| tp i = transport-filler (λ i → X i) a i | ||
|
|
||
| bottom : (i : I) → X i | ||
| bottom i = pd (x i0 1=1) (x i1 1=1) i |
There was a problem hiding this comment.
There was a problem hiding this comment.
There is also https://github.com/agda/cubical/blob/master/Cubical/Foundations/Path.agda#L130 which might be the next dimension, but I did not think hard about it...
There was a problem hiding this comment.
It's exactly extend₁ with ϕ = j ∨ ~ j. But it seems a bit hard to generalize this argument to higher dimensions...
There was a problem hiding this comment.
Can you use https://github.com/agda/cubical/blob/master/Cubical/Foundations/Prelude.agda#L548 here?
Ok.
|
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 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 |
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 |
* done * fix Everything * update * add an example * fix * typos * alignment
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...