HoTT/HoTT — pull request #492 by JasonGross (2014-09-11 18:33:11+00:00)
Title: Fix frudenthal, reorder Truncation_functor args

It seems that I didn't rebase enough before the frudenthal fix was merged. Some of the reorganization in Truncation broke some things, which are not fully fixed.

Now, when you [apply Truncation_functor], you're not left with a goal of
[Univalence]. However, this isn't a satisfactory solution; perhaps
@mikeshulman can help solve the remaining goal involving
[truncation_incl] and [Truncation_functor] which used to go through
judgmentally?