2-Adjoint Equivalences in Homotopy Type Theory