Merge pull request #375 from JasonGross/set-notation

Define Type0 to mean Set
Fix the universes of some HITs; add a check file

Susp X is now in the same universe as X.

This is verified in the Tests.v file.

This closes #369.

It's possible we should fix the universes of quotients, but this will be
trickier.  In trunk-polyproj, we can do it like this:

```coq
Section Domain.
Let U := Type.
(** We need a universe level that is not lower than [U], but doesn't
need to be the same. *)
Let U' : Type.
Proof.
  let U' := constr:(Type) in
  let U_le_U' := constr:(fun x : U => (x : U')) in
  exact U'.
Defined.
Context {A : Type} {R:A -> A -> U} {sR:setrel R}.

Inductive quotient (sR:setrel R): U' :=
 | class_of : A -> quotient sR.
```

But in HoTT/coq, this gives "Error: No such section variable or
assumption: U'." at `End Domain.` (see
https://github.com/HoTT/coq/issues/116).