HoTT/HoTT — pull request #563 by mikeshulman (2014-10-09 06:56:21+00:00)
Title: Factorization systems

Of course, this is preliminary to constructing the connected/truncated factorization system for any modality.

This file is twice as slow to compile as the previously slowest file (namely `V.v`). Adding explicit universe annotations sped it up by a couple of seconds already. Any other suggestions would be welcome.