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 don't fully understand it, but here's some more output which might or might not suggest something more subtle:
```coq
Section same.
  Universe i.
  Variables A B : Type@{i}.
  Definition foo := A -> B.
End same.
Definition bar := Eval compute in foo = foo -> Type@{i}.
Section different.
  Variables A B : Type@{j}.
  Definition foo' := A -> B.
End different.
Definition bar' := Eval compute in foo' = foo' -> Type@{h}.
Set Printing Universes.
Print bar.
(* bar =
(fun A B : Type@{i} => A -> B) = (fun A B : Type@{i} => A -> B) -> Type@{i}
     : Type@{max(i+1, Top.367)}
(* Top.367 |= Top.358 < Top.367
                *) *)
Eval compute in (fun _ => Type) : @bar@{Set}.
Print bar'.
(* bar' =
(fun A B : Type@{Top.372} => A -> B) = (fun A B : Type@{Top.372} => A -> B) ->
Type@{Top.374}
     : Type@{max(Top.371, Top.374+1)}
(* Top.371
   Top.372
   Top.374 |= Top.372 < Top.371
                *) *)
Eval compute in (fun _ => Type) : @bar'@{j Set k}. (*      = fun _ : (fun A B : Set => A -> B) = (fun A B : Set => A -> B) =>
       Type@{Top.383}
     : bar'@{Top.381 Set
Top.382} *)
```
I'm still a bit confused by it, but I'm starting to think you might be right.