Speed things up by nearly a factor of 2

This idea is due to Matthieu Sozeau; it eliminates a number of
universes, vastly reducing hashconsing.  The 20x speedup in
categories/Pseudofunctor/RewriteLaws is amazing!

```
After    | File Name                                                          | Before   || Change
-----------------------------------------------------------------------------------------------------
3m24.28s | Total                                                              | 6m10.15s || -2m45.87s
-----------------------------------------------------------------------------------------------------
0m05.96s | categories/Pseudofunctor/RewriteLaws                               | 1m01.75s || -0m55.78s
0m21.92s | categories/Comma/ProjectionFunctors                                | 0m37.20s || -0m15.28s
0m05.35s | categories/Grothendieck/PseudofunctorToCat                         | 0m19.98s || -0m14.63s
0m00.96s | categories/PseudonaturalTransformation/Core                        | 0m11.24s || -0m10.28s
0m07.10s | categories/Comma/InducedFunctors                                   | 0m14.42s || -0m07.32s
0m10.84s | categories/ExponentialLaws/Law4/Functors                           | 0m17.52s || -0m06.67s
0m02.59s | categories/Yoneda                                                  | 0m08.62s || -0m06.02s
0m05.04s | categories/Adjoint/HomCoercions                                    | 0m08.23s || -0m03.19s
0m00.50s | categories/Pseudofunctor/Core                                      | 0m03.84s || -0m03.33s
0m09.65s | categories/Adjoint/Dual                                            | 0m12.34s || -0m02.68s
0m09.05s | categories/Adjoint/Composition/AssociativityLaw                    | 0m11.26s || -0m02.20s
0m02.92s | categories/Adjoint/UniversalMorphisms                              | 0m05.02s || -0m02.09s
0m02.18s | categories/Pseudofunctor/FromFunctor                               | 0m05.04s || -0m02.85s
0m00.96s | categories/Limits/Core                                             | 0m03.50s || -0m02.54s
0m00.94s | categories/Functor/Composition/Functorial/Attributes               | 0m03.46s || -0m02.52s
0m03.79s | categories/UniversalProperties                                     | 0m05.68s || -0m01.88s
0m03.31s | categories/Pseudofunctor/Identity                                  | 0m04.88s || -0m01.56s
0m02.81s | categories/Comma/Dual                                              | 0m04.02s || -0m01.20s
0m01.77s | categories/ExponentialLaws/Law1/Law                                | 0m03.08s || -0m01.31s
0m01.09s | categories/ExponentialLaws/Law2/Functors                           | 0m02.13s || -0m01.03s
0m01.03s | categories/Functor/Composition/Functorial/Core                     | 0m02.48s || -0m01.44s
0m00.93s | categories/Functor/Prod/Functorial                                 | 0m02.45s || -0m01.52s
0m00.76s | categories/ExponentialLaws/Law  N/A                                | 0m01.92s || -0m01.15s
0m00.54s | categories/NaturalTransformation/Pointwise                         | 0m01.55s || -0m01.01s
0m00.38s | categories/Limits/Functors                                         | 0m01.50s || -0m01.12s
0m08.11s | categories/FunctorCategory/Dual                                    | 0m09.08s || -0m00.97s
```