Feature request: pattern matching on identity path about cubical HOT 7 CLOSED

Haha ok, please do this after finishing the paper then :-)

from cubical.

There are 1252 uses of refl (counted with "cat *agda | grep -c refl") and so it is not an option to replace all of those which happen to be patterns (the vast majority) by uses of J (or equivalent cubical machinery) manually.

I wanted to test the performance of univalence as computed by cubical Agda with my code, but this is preventing me from doing so.

from cubical.

Yes, this would be great to have. But as this is not a feature request for the agda/cubical library but rather for agda maybe we should discuss it in an issue there instead?

from cubical.

Yes, sorry, I put my request in the wrong cubical compartment! I will make the request there,

from cubical.

@martinescardo Did you make an issue over at Agda? If so I'll close this one

from cubical.

Not yet, but you can close it. I am trying to finish a paper, and I am late for the extended deadline I got. :-)

from cubical.

Done. Haven't finished the paper, though. :-)

agda/agda#3551

from cubical.