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.
Indeed, Universe is not polymorphically discharged yet, I hope to get back to this and the general naming system for universes soon. There is an unsolved issue with discharging and universes though, what should happen when you have a "polymorphic" universe section variable that is discharged on a monomorphic definition... I suppose we should make it polymorphic on just that variable but then one would need to distinguish the polymorphic and global universes and constraints associated to each definition. I'd be tempted to forbid this case. When the universe section variable is global there is no problem I think, it stays declared outside the declared section definitions whatever their universe polymorphism status is.