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.
I tried that first.  `Local Universe i` gives `Error: This command does not support Locality`.  Plain `Universe i` seems to be global even if it's in a section.