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.
Do you want to do this in this PR, or in another PR?