Resolve duplicate definitions

[VojtechStep]

We aim to have unique identifiers for all public definitions throughout the codebase, as stated in the library coding style guide. This was supposed to be enforced by recursively opening all modules of the library, so that Agda would complain about duplicate definitions when checking the Everything file.

Unfortunately we aren't properly opening the top-level modules, so while we avoided naming collisions inside top-level modules, we managed to introduce duplicates across top-level module boundaries. These should be resolved by either removing one of the definitions, and reusing the other, or by renaming one or both definitions to something less ambiguous.

So far I found the following duplicates:

• Theory of finite groups is duplicated between finite-algebra and finite-group-theory. The finite-algebra module should build on top of the formalization from finite-group-theory
• foundation.separated-types.is-separated vs orthogonal-factorization-systems.separated-types.is-separated
• univalent-combinatorics.standard-finite-types.Fin vs reflection.group-solver.Fin
• universal-algebra.terms-over-signatures.Term vs reflections.terms.Term
• foundation.path-algebra.cube vs univalent-combinatorics.cubes.cube

The Everything file is generated by a script in the Makefile, so once the duplicates are resolved, we should change the script to generate open import <module> public lines.