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

Add proof for adjointification (only need to provide a quasi-inverse to construct an equivalence) and prove that the inverse of an equivalence is an equivalence.