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.
I just tried it, and that works with one caveat: anyone who uses `merely` or `hexists` needs to import `TruncType` in order to get the coercion.  It seems like that would result in confusion, if you only need to import `hit.Truncations` in order to _see_ `merely` and `hexists`, but you need to import something else in order to use them correctly.

One option would be to move the _definition_ of `TruncType`, along with its notations, coercions, etc., into somewhere like `Basics/Trunc` (or even `Overture`).  The rest of the file `TruncType` depends on `types/Universe`, but the definition and coercions don't, and there's some precedent for putting definitions early and then proving things about them later on after we have more tools (e.g. `Empty` and `Unit` are defined in `Overture` rather than their `types/` files).