Add two more kinds of duals

The identifiers L and R refer to which ^op is removed/inverted.
Functorialize yoneda

Alas, I still don't really understand the Yoneda lemma.

Also, the proof is very long.  I'd be happy if anyone could clean it up.

After    | File Name                          | Before   || Change
---------------------------------------------------------------------
0m08.45s | Total                              | 0m07.85s || +0m00.59s
---------------------------------------------------------------------
0m04.29s | categories/Adjoint/HomCoercions    | 0m04.00s || +0m00.29s
0m02.39s | categories/Yoneda                  | 0m02.28s || +0m00.11s
0m00.64s | categories/SetCategory/Morphisms   | 0m00.43s || +0m00.21s
0m00.43s | categories/categories              | 0m00.40s || +0m00.02s
0m00.41s | contrib/HoTTBook                   | 0m00.47s || -0m00.06s
0m00.18s | categories/Adjoint/Adjoint         | 0m00.18s || +0m00.00s
0m00.12s | categories/SetCategory/SetCategory | 0m00.10s || +0m00.01s
Fix a typo in the cat-timing-files script
Merge pull request #421 from JasonGross/finished-but-slow-yoneda-unified

Functorialize the yoneda lemma

LGTM
WIP
WIP
WIP
WIP
WIP
WIP
Improve Comma/Dual.v
WIP
WIP
WIP
WIP