leanprover/lean — pull request #320 by javra (2014-11-14 21:02:55+00:00)
Title: feat(library/hott) funext_from_ua.lean almost done

What's missing is to fix the universes, but I guess we have to start fixing path.lean and trunc.lean