Adjoint equivalences preserve colimits

[Taneb]

I feel it should be possible to show a weaker version of this, that if C -| D then R preserves limits and L preserves colimits. c.f. https://ncatlab.org/nlab/show/adjoints+preserve+(co-)limits (which would justify the feeling of the author of Categories.Category.Finite that the right adjoint is enough there)

[Taneb]

I've realised that I've misunderstood something here. This module is not preserving limits, but preserving the diagram of limits. Not sure how I want to proceed (but it explains why I kept getting things backwards)

[JacquesCarette]

The code all seems fine, but I get from your comment that this isn't ready to merge? Or this is, but additional code that you were thinking of doing isn't?

[Taneb]

Issues:

1. This isn't what "preserves limits" normally means and I shouldn't have renamed the proof that
2. I don't know a good name for it otherwise that has a corresponding name for the colimit case
3. I don't really get how this relates to Category.Finite so I don't know how the comment there should be adjusted
4. The proof doesn't need adjoint equivalence, a simple adjunction will do (I have a proof of this locally, which I can make a PR for once the previous points are resolved)