Splitting of coherent idempotents

An answer to a question of Martin Escardo.
`HoTT.v` does not export all files without axioms.  For example, there are many in categories that it does not export, and it exports `HoTT.Types`, not every file in the types directory.  Similarly, if we were to make `DerivedTypes/Cantor/Core.v` and `DerivedTypes/Cantor/Idempotent.v` and  have `DerivedTypes/Cantor.v` `Export DerivedTypes.Cantor.Core` and `Import DerivedTypes.Cantor.Idempotent` and, say `Export DerivedTypes.Cantor.Idempotent.ImportantResults` (with the nicely named results in `Module ImportantResults` at the bottom of `Cantor/Idempotent.v`), then `HoTT.v` could just `Export DerivedTypes.Cantor`.