Merge pull request #371 from JasonGross/empty-is-set

Make Empty a Set
Put quotient in the right universe

It's a pain.
Add a note about moving to trunk-polyproj/8.5