Prove converse of a result on adjunctions

[mortberg]

See comment on https://github.com/UniMath/UniMath/pull/606#issuecomment-282258761. This could be a nice exercise for someone who wants to learn UniMath.

[langston-barrett]

I wonder if an even stronger result holds: that there is a weak equivalence between such "natural weak equivalences of hom-types" and adjunctions. I.e. this logical equivalence might be a a full weak equivalence.

[m-lindgren]

I think this can be closed. Fixed by #950 and #952.

[benediktahrens]

@m-lindgren : thanks for finding this - closing.