pi3js2

Results 2 issues of pi3js2

[note: in the latest, the `erp` operator has been renamed to `interpolateI` and is defined in `Cubical.Core.Interpolate`] Here I added an "interpolation" operator on the interval, in Cubical.Foundations.Erp: ```agda erp...

Here is a performance mystery seemingly involving `unglue`. I wonder if I just did something bad? The mystery is at the bottom. Typechecking the last definitions (commented) takes a very...