Turn off η-equality by default

[fredrik-bakke]

No description provided.

[VojtechStep]

I think this needs some documentation on how eta equality is used in the library and what are the consequences. One non-obvious consequence of this change is that if you don't turn on eta-equality and just write a record, you will not be able to prove propositional eta either (and consequently you can't prove that the record is equivalent to an iterated sigma). The only way to do that in non-cubical Agda is to enable pattern for the record, at which point it becomes a positive type — you can only pattern match on the constructor, but you can't define values by copattern matching.

Personally I'd prefer to go the other direction — have eta by default, but apply no-eta-equality generously, always accompanied with some comment on the fact, like "this is supposed to be a top-level container that we don't decompose and unify", or "this could have eta equality, but disabling it led to performance gains here and here". I think having these notes would hopefully make this feature less folklore-heavy (or at least make the folklore explicit with examples).

BTW with this change I can reproduce ~1.8% improvement in type checking time, 8m18s -> 8m9s, nice 👍