feat(library/hott) add proof of 'adjointification'

This theorem establishes that is suffices to give a quasi-inverse to establish an equivalence.