Evan Cavallo
Evan Cavallo
@kangrongji, are you willing to rewrite to move the dependency on natural numbers into the reflection? Alternatively, a stopgap solution that would work for 2.6.3 (but not the glorious future)...
OK, thanks!
Same here, I don't know the problem.
Now the button to run CI appeared. Not sure what changed, but I clicked it.
@andreasabel asked me if I had any project that uses rewrite rules. Here is one: https://github.com/ecavallo/equivariant-cartesian
I went ahead and made some changes, particularly to prefer copatterns over record syntax where it's not too inconvenient and to make some type signatures more explicit. Does everything look...
Thanks for the contribution (and sorry for the long wait)!
At least as far as semantics is concerned, there's no problem with `I` in parameters.
> Indeed, calling it `interp` or `interpolate` sounds good to me. Otherwise I think this could be merged? @ecavallo Any opinions? Looks good to me.
(Mentioned this on Discord, repeating here for the record) We added a definition of `pathToEquiv` to the library with the intent of removing it from Agda.Builtin.Cubical: https://github.com/agda/cubical/issues/259. Is there anything...