Finish non-dep functoriality of adjoints

With some help from Mike Shulman on #627 and #629, I've managed to
finish the construction that shows that the construction of adjoint
functors is functorial in its functor argument.  I've not yet managed to
extend this to the dependent case as an assembled functor, though the
individual parts all have dependent versions.

This closes #629.
What's this again? It does not appear to be documented.
https://coq.inria.fr/refman/command-index.html