Use an assumption rather than a flag for WithK?

[ecavallo]

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 we want to keep a proof that K is inconsistent in the libary, we could rewrite the file as a module that depends on an assumed proof of K. Then no special treatment is needed (and the file might be more useful, for example if we wanted to show that something else implies K and is therefore inconsistent).