Anders Mörtberg

What we do in cubicaltt for opaque/transparent is not safe and was never meant to be. It is easy to see that you can break subject reduction using it. It...

Oops, I wrote something stupid in a comment that I deleted. Sorry for the noise.

Indeed. We should document them and say that they are experimental.

I made some tests and this doesn't seem to make things faster... I ran testShortcut4To5 (after applying https://github.com/mortberg/cubicaltt/commit/7d70bea5a8d9c540c6b0a765a62e4f43f612ff7b) and the timing is actually 1s slower.

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

Yeah, test0To5 definitely needs to get faster. However f8 (kappaTwo) seems to cause a massive combinatorial explosion. Try the following: ``` > :n f7 (f6 (f3 test0To2)) ... > :n...

> Oh yeah a direct proof of `kappaTwo` will be awesome. The map is defined in B.10 (page 155) of https://arxiv.org/pdf/1606.05916.pdf Maybe someone can come up with a more efficient...

> > Oh yeah a direct proof of `kappaTwo` will be awesome. > > The map is defined in B.10 (page 155) of https://arxiv.org/pdf/1606.05916.pdf > > Maybe someone can come...

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

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