3abc

> Can you redo the redtt experiment with iterated path types so that we can see if it's the extension types that are helping or not? An obvious difference is...

> redo the redtt experiment with iterated path types I just did. Now it's a lot slower. 5d-cube took 60 seconds, and I expect 6d-cube to take 20 minutes and...

The [6d-cube](https://gist.github.com/3abc/e3191e09bf384ea7bed2bfbf8822c2dd) for redtt is not done yet, after 100 minutes. So maybe it will take days for 7d-cube to run (given that 5d -> 1 minute, 6d -> at...

> I think the conclusion of this experiment is that we need extension types in Cubical Agda. These are not only great from the point of view of efficiency; they...

And I can see how extension types are simpler both homotopically and combinatorially. After all assembling a 4d-cube from a 3d-base + 6 3d-sides is simpler than from 16 vertices,...

> @ecavallo has some alternative definition of this map that completely avoids the lemmas that this patch affects, however this doesn't seem to make things faster either. So the strange...

> I think the problem might be that we are running `truncPath2` to compute the path that we are transporting in, and this might end up being extremely complex. Another...

> Evan seems to have figured it out: #110 > > Those new maps seem to have linear complexity in the number of hcomps in the input. This is a...

> PS: the idea to hopefully optimize f5 is to use Loic's definition of the map from the total space of the Hopf fibration to S1 * S1 instead of...

> Wow, this should be better in Cubical Agda then... Once we have a perfected version of f5 it should be fairly straightforward to port the definition and try it...