Factorization systems

Of course, this is preliminary to constructing the connected/truncated factorization system for any modality.

This file is twice as slow to compile as the previously slowest file (namely `V.v`).  Adding explicit universe annotations sped it up by a couple of seconds already.  Any other suggestions would be welcome.
Gah.  @mattam82, can you fix this?  (Should we report a bug?)

@mikeshulman, what suggests that it's global, other than `Print`ing the definition?