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.
Add id Adjunction.  Also, infixr _\o_