feat(category_theory/adjunction): adjoint lifting theorems (#5118)
Proves the [adjoint lifting theorem](https://ncatlab.org/nlab/show/adjoint+lifting+theorem) and the [adjoint triangle theorem](https://ncatlab.org/nlab/show/adjoint+triangle+theorem).
The intent here is for all but the last four statements in the file to be implementation.