Proving Eliminators without using J.

[3abc]

I used a lemma called g2TruncFib similar to setTruncFib.

Just one remark, for g2TruncFib (and similarly setTruncFib) to work we don't need that gP x is a 2-groupoid for all x. We actually only need it to be a 2-groupoid at the fiber over b. However I choose to keep the type unchanged. But this could be useful at some point where not all fibers are known to be 2-groupoid.

[mortberg]

I made some tests and this doesn't seem to make things faster... I ran testShortcut4To5 (after applying 7d70bea) and the timing is actually 1s slower.

[mortberg]

@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 in the latter maps doesn't seem to come from this.

[3abc]

@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 in the latter maps doesn't seem to come from this.

I think the most time consuming part is from the map h sending test0To4 to test0To5? At least on my computer I can't have cubicaltt to compute normal form of test0To5. For that I think we either need to greatly simplify the proof of decodeEncode or find a direct proof of a special case of isSet loopS1

setLoopRefls : (r : Path loopS1 refl refl) → r ≡ refl

The part that using g2TruncElim is f7 sending test0To6 to test0To7, I think it's already kinda fast in cubicaltt if the input is not too complicated? Like testShortcut3To6 shows. However this version of g2TruncElim can be really useful in Agda, at least it greatly simplifies normal form of things like multTwoTilde base2 (g2squashC x y p q r s u v i j k l). For the version using J it was 400k lines and 20 min, for this version it's almost instant.

[mortberg]

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 f8 (f7 (f6 (f3 test0To2)))
...
> :n f8 (f7 (f6 (f3 (f6 (f3 test0To2)))))
...

This map seems very innocent so I wonder what is going on. 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 definition of this map could speed things up a lot in the latter part of the computation.

[3abc]

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 definition of this map could speed things up a lot in the latter part of the computation.

Oh yeah a direct definition of kappaTwo will be awesome.

[mortberg]

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 definition? @ecavallo @loic-p

The case we need here is n=2 and A=S^2.

[mortberg]

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 definition? @ecavallo @loic-p

The case we need here is n=2 and A=S^2.

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 huge improvement to f8-f10 that were seemingly at least exponential.

The next step is to optimize f5. I have some ideas for how to do it, but I really have to work on a grant proposal so it might be a few weeks before I work on it

[mortberg]

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 "tee" map (https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L925):

https://github.com/agda/cubical/blob/master/Cubical/HITs/Hopf.agda#L60

As Loic's map is defined for the Hopf fibration defined using the suspension of S1 we will have to change a bunch of other things in f5 as well. One way to quickly test it might be to insert the map:

https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L927

somewhere but I'm not sure where. If someone experiments with this please keep me posted.

[3abc]

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 huge improvement to f8-f10 that were seemingly at least exponential.

Just one observation: I just did :n (g9 (g8 (f7 (f6 (f3 test0To2))))) and there's a lot of empty systems. However it doesn't cause much problem since after applying g10 they all disappear.

NORMEVAL: hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z)

[...] (the full term has 13.3K characters, use option -f to print it)

]) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []
#hcomps: 604
Time: 0m0.065s

[mortberg]

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.

[3abc]

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 "tee" map (https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L925):

https://github.com/agda/cubical/blob/master/Cubical/HITs/Hopf.agda#L60

Is there any heuristic for one to believe this new map is better than the one defined by tee?

[mortberg]

Is there any heuristic for one to believe this new map is better than the one defined by tee?

I seems simpler and shorter. But this is very hard to judge without trying, so we will have to see empirically :)

[3abc]

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.

I used -f and it turns out to be just (sinc (pos (suc zero))) with 604 empty systems...

[mortberg]

Is there any heuristic for one to believe this new map is better than the one defined by tee?

I seems simpler and shorter. But this is very hard to judge without trying, so we will have to see empirically :)

I ported it now:

https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L972

It doesn't seem faster... But more testing and experimenting is necessary.