Adjoints preserve diagrams

[Taneb]

Supersedes #454 and, to me, justifies removing Categories.Adjoint.Equivalence.Properties entirely, as ⊣equiv-preserves-diagram is a special case of la-preserves-diagram (along with sym).

The proof is mostly the same as in Categories.Adjoint.Equivalence.Properties, apart from !cone.commute, which takes a different route. (I suspect the author of that module seeing that proof before this proof was what led them to believe the equivalence was necessary)

Discussion points:

• Are these names good enough?
• Is this the right module to put these laws in?
• Should we remove Categories.Adjoint.Equivalence.Properties now?
• What should we do about the comment in Categories.Category.Finite?

[JacquesCarette]

• do we use 'la' and 'ra' anywhere else? I think I've seen LAdj and RAdj?
• yes
• yes
• they probably need a thorough review. I've never been fully convinced with that definition (but I'm still searching for a good definition of Finite, so it's deeper than just this code, which wasn't mine.)