HoTT/HoTT — pull request #402 by mattam82 (2014-06-10 16:14:21+00:00)
Title: Make the core and a bit of categories compile with the current trunk.

The main changes are Private for Local Inductive types for HITs and
a change in the handling of axioms univalence and funext:
Now they are fully polymorphic and take a dummy argument to pinpoint
their uses (as in Agda's library I think).

This is not a serious pull request, the patch is not clean, although some parts could
be picked already. Or should I make it to another, unstable branch of HoTT/HoTT?

There are a few places where unification is doing arbitrary choices which I don't like,
infering identity functions where others apply, but I guess it's safe to just specify them.

It's unclear to me why the definition in Functor/Attributes gives an inconsistency, and even more so, why Set suddenly appears there, maybe @jasongross can figure it out?

The current trunk allows level specifications, I started using build explicit lifts of inductive definitions like paths, IsTrunc etc... but the solution where univalence and funext are fully polymorphic doesn't require it. Only in Modality did I need it to ensure that levels wouldn't fall down to Set due to minimization. Anyway, take what you like :)

I'd like to get a clean view of what remains broken now. Is it all the HoTT test-suite files that are in trunk now @JasonGross ?