leanprover/lean — pull request #312 by fpvandoorn (2014-11-09 02:15:29+00:00)
Title: feat(library/hott/trunc) extended truncation library

I've ported most of the contents of `Trunc.v` in Coq HoTT to `trunc.lean`.