Add id Adjunction
Implement composition of adjunctions

Perhaps composition should be moved to a separate file; this proof takes
up about 1.5 GB RAM and takes around 10-30 minutes to typecheck, on my
machine. The construction was copied from AdjointComposition.v at
https://bitbucket.org/JasonGross/catdb.