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.
Yes, I agree: at least the part of the proof that comes before opening long_path_scope ought to benefit from the sort of automation we were discussing in the other issue.  Whenever we get around to working on that, this should be a good test case.