HoTT/HoTT — pull request #148 by JasonGross (2013-07-10 08:00:46+00:00)
Title: Make BuildEquiv a coercion

This way, things of type IsEquiv can turn into things of type Equiv.