Global Set Primitive Projections

This is on top of #638.

```
Idempotents got waay faster, though Factorization got somewhat slower.
Not quite sure what's up with that.

After    | File Name                                                 | Before   || Change
--------------------------------------------------------------------------------------------
3m47.71s | Total                                                     | 4m20.05s || -0m32.33s
--------------------------------------------------------------------------------------------
0m01.88s | Idempotents                                               | 0m30.73s || -0m28.85s
0m16.40s | Factorization                                             | 0m05.88s || +0m10.51s
0m17.75s | hit/V                                                     | 0m21.02s || -0m03.26s
0m02.78s | Modalities/Modality                                       | 0m06.33s || -0m03.55s
0m50.97s | categories/Adjoint/Pointwise                              | 0m53.29s || -0m02.32s
0m02.58s | Basics/Equivalences                                       | 0m00.66s || +0m01.92s
0m01.71s | categories/ExponentialLaws/Law1/Law                       | 0m02.71s || -0m01.00s
```

@mattam82, do you have any updates on [bug 3709](https://coq.inria.fr/bugs/show_bug.cgi?id=3709) and [bug 3782](https://coq.inria.fr/bugs/show_bug.cgi?id=3782)?  Should we wait for these to be fixed, or merge this as-is?

The slowest bits in the new version of `Factorization.v`:
```
0.371 secs Chars 135 - 191 [Require~Import~HProp~Univalenc...] (0.008u,0.328s)
0.823 secs Chars 96 - 134 [Require~Import~HoTT.Basics~HoT...] (0.016u,0.632s)
4.466 secs Chars 7989 - 7993 [Qed.] (4.444u,0.024s)
4.758 secs Chars 9818 - 9822 [Qed.] (4.752u,0.008s)
5.525 secs Chars 9849 - 9867 [End~Factorization.] (5.512u,0.012s)
```
The slowest bits in the old version (from before set keyed unification):
```
0.311 secs Chars 9682 - 9704 [End~PathFactorization.] (0.312u,0.s)
0.894 secs Chars 7845 - 7849 [Qed.] (0.896u,0.s)
0.933 secs Chars 9705 - 9723 [End~Factorization.] (0.92u,0.008s)
1.038 secs Chars 9674 - 9678 [Qed.] (1.04u,0.s)
1.365 secs Chars 135 - 191 [Require~Import~HProp~Univalenc...] (0.008u,0.304s)
3.009 secs Chars 96 - 134 [Require~Import~HoTT.Basics~HoT...] (0.032u,0.72s)
```
I suspect this is an issue in the order chosen in the conversion algorithm.