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.)

[Taneb]

Regarding la and ra as prefixes, I was mostly going off lapc and rapl. We also just use L or R, which I like even less

[JacquesCarette]

Wasn't it LAPC and RAPL? I agree that a raw L (or R) is too short. I'm just wondering about capitalization at this point!

[Taneb]

The module is called RAPL, but the definition is rapl