The file simpson-delooping-sign-homomorphism does not compile with --experimental-lossy-unification

[EgbertRijke]

It runs into universe problems, indicating that there is something off with the file. Some lemmas are extremely long, and it is also one of files that takes longest to compile.

[EgbertRijke]

Note: this is a new file, incoming with the current pull request. It contains stuff that was previously in the file sign-homomorphism.