fix(library/hott) close gaps and clean up adjointification proof