More adjunctions

I've copied over some types from Functor.agda and NaturalTransformation.agda and proven analogous things about adjunctions.  I've also reorganized it into a few different files.  Feel free to rename either of the files I put in `Adjunctions/` before merging this.  I'd also appreciate feedback about style (and anything else).