Add some typeclass glue to FunextVarieties
Remove dependencies on HoTT.v

Also include more things in HoTT.v and fix up some other dependencies.

This closes #322.
Merge pull request #333 from JasonGross/fix-hott-deps

Remove dependencies on HoTT.v
Merge pull request #331 from JasonGross/funext-glue

Add some typeclass glue to FunextVarieties
Circle was in Prop.  Now it's not.

Instead it's in Set, which is fine.  Also, fix definition of eliminator
as per #122.