Category no eta equality

[maxsnew]

Implementing #1240 . Haven't been able to test locally because checking Cubical.Categories.Instances.CommAlgebras seems to hang

[mortberg]

Did you try adding --lossy-unification to the slow files?

[maxsnew]

The comment I made is out of date. This PR is actually ready to merge. I had meant to do some performance numbers before we merge. Rebuilding the entire library from scratch the difference was negligible (~0.9% improvement) but I was able to remove one --lossy-unification.

[mortberg]

Ok, did you notice any speedup for your library? I can't help but wonder if this change is necessary if the speedup is negligible. Having C^op^op = C definitionally is definitely nice to have, but the prize to pay for removing it doesn't seem so big either.

[maxsnew]

We haven't fully ported our library yet but we have been able to remove some uses of --lossy-unification.

The negligible performance difference is across the entire cubical
library, of which the Categories portion is a small part. This morning
I ran some more direct benchmarks: I ran make on the entire library
and then I deleted _build/2.8.0/Cubical/Categories and re-ran
make, so that we are only testing how long building the portion of
the library that depends on Categories is. I also ran a baseline of
just how fast running make a second time was to test just how long
checking all of the caching takes to set a baseline. Here are the numbers:

With no-eta-equality (i.e., this PR):

1. Baseline: 25s
2. Rebuilding Categories: 116s

Without eta-equality (i.e., the starting point for this PR) :

1. Baseline: 24s
2. Rebuilding Categories: 130s

So there's about a 14s improvement, i.e. a ~10.7% improvement on total
runtime (14/130). If you remove the baseline, this is ~13.2%
improvement (14/106).

There's some confounding factors of course. I removed a --lossy-unification in Functors.ComposeProperty.agda, but I also instantiated an implicit argument explicitly in Cubical/Categories/Instances/CommAlgebras.agda.

[mortberg]

Ok, that's more convincing! Thanks a lot. If we can notice a 10% speedup already for the very moderate amount of CT that we have in the library now I would expect this to make even more of a difference if that part of the library grows. So I'll merge this now.

Maybe this is good evidence that it's worth going through the pain of doing the same change for the algebraic structures @felixwellen ...