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.
Just printing the definition.

```
Section Foo.
  Universe i.
  Definition A : Type@{i}.
  Admitted.
End Foo.
Set Printing Universes.
Print A.
```

gives

```
*** [ A : Type@{i} ]
```

while leaving out the `Universe i` command gives

```
*** [ A : Type@{Top.31} ]
(* Top.31 |=  *)
```

I assumed that the lack of a comment like `(* i |= *)` in the first output meant that `i` was still assumed as a fixed global universe, but I guess I could be wrong about that.