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.
Not as much of one as I'd like.  Once we `Set Keyed Unification`, it becomes possible to do these with `match goal with context [ ... ] => rewrite ... end` so that at least the tactic script doesn't have to record the exact place of the lemma inside a nested path composition.  And we could wrap that up in a tactic so the user doesn't have to see it.  But I don't know why plain `rewrite` doesn't work; I brought it up at #553 .