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.

I'd appreciate any comments/criticism/suggestions, on style, or otherwise; this is the first agda code I've written which is more than ~10 lines long.