HoTT/HoTT — pull request #566 by mikeshulman (2014-10-11 05:01:39+00:00)
Title: make hSet and hProp special cases of TruncType

This means any file that uses the universes `hProp` and `hSet` now has to import `TruncType`. I also moved a few things around to more logical places, e.g. the facts about hprops that use univalence can and must go in `TruncType` now, and some things from `Misc` went elsewhere. Also, somehow `HoTT` wasn't exporting `TruncType` before.

There are two things I'm not entirely happy with, but haven't thought of a better solution for:

1. In order to leave `ismono` in `HProp` rather than moving it to `TruncType`, I had to unbundle the hypothesis. In general this is not a problem, but it made for a bit of ugliness in `categories/Functor/Attributes` since `ismono` is no longer definitionally the same as `IsMonomorphism` in the category of sets.

2. There was a `Canonical Structure` in `HSet.v`, despite our general principle of avoiding them. I left it in (and in fact generalized it to all `n`), because a handful of places in `categories` seem to depend on it. I'd prefer to remove it, but I wasn't able to find a clean-looking way to fix categories.