Evan Cavallo
Evan Cavallo
Not sure if this is a good idea. Sometimes I'm defining a cube and for whatever reason it's more convenient if I flip it along some diagonal first. I could...
``` import path import J data vacu where | more (x : vacu) let Code (m : vacu) (n : vacu) : type = elim n [ more n' =>...
``` data unit where | triv opaque let t : (A : type) × A = (unit, triv) let a = t .snd ``` raises `Failure("popl: empty")`. Writing ``` let...
The eliminator for a HIT takes `fhcom`s to `com`s in the target type. When the motive is non-dependent, the output `com` is in a constant line, so the desired behavior...
It doesn't have anything to do with reflection (don't know why I put it there in the first place) and is generally useful. The obstacle is that different functions called...
Resolves #830. This way we don't have a file that relies on an extra flag and isn't usable in the rest of the library (and needs its own special case...
Just for simplicity and accuracy. [The contents](https://github.com/agda/cubical/blob/master/Cubical/Functions/FunExtEquiv.agda) aren't all equivalences.
https://github.com/agda/cubical/blob/master/Cubical/WithK.agda Is it essential that we demonstrate the incompatibility of `--cubical` and `--with-K` in the library? Currently we have a special case in the Makefile just for this file. If...