HoTT/HoTT — pull request #623 by mikeshulman (2014-11-24 19:30:42+00:00)
Title: trunc_leq transparent & not an instance, no no-ops in trunc_contr

Also illustrates the fragility of universe annotations: changing the configuration of `IsTrunc` instances caused `ishprop_ooextendable` to take one fewer universe parameter. Interestingly, results in a noticeable speedup, perhaps from smaller `IsTrunc` instances or fewer universes.