leanprover/lean — pull request #254 by javra (2014-10-24 22:52:58+00:00)
Title: feat(library/hott) add proof of 'adjointification'

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