HoTT/HoTT — pull request #417 by JasonGross (2014-07-24 11:15:20+00:00)
Title: 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
```