Adjunctions (notions of adjunctions)

[emilyriehl]

I started defining some of the adjunction data enumerated in #26. I'm pushing now so that this can be used for the development of limits and colimits (which is underway). There's a lot of work still to be done!

I attempted to follow the naming conventions of the style guide but would appreciate a second opinion.

As auxiliary functions I also

• defined a primitive quadruple-comp function in our common file.
• defined whiskering of natural transformations (as a special case of horizontal composition) in the 2-cats file.
• defined coherence data I'm referring to by the name of "Gray-interchanger".

The Gray-interchanger is a commutative square, built by gluing two hom2 terms together. I refer to one of these as "left" and the other as "right" for lack of obvious better names.

[fizruk]

Looks great! I would only suggest to change ladj and radj into left-adj and right-adj everywhere.

[emilyriehl]

@fizruk it looks like I can't review my own pull request. The new commit just makes the requested notation change.