leanprover/lean — pull request #255 by javra (2014-10-25 01:00:10+00:00)
Title: 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.