improve "make clean" and change some identifier names

  make "make clean" remove all *.vo and *.glob files, even the unknown ones

  change some identifier names to obey the convention that types are capitalized
  and objects are not.  Also change HProp, HSet, Trunc to IsHProp, IsHSet, IsTrunc.
improve proof of isprop_biinv
Fixing HProp
Merge branch 'pull-request-2' of https://github.com/DanGrayson/HoTT into upstream

Conflicts:
	theories/Equivalences.v
more capitalization
Merge branch 'pull-request-2' of https://github.com/DanGrayson/HoTT

Fixing Conflicts:
	theories/Equivalences.v
	theories/HProp.v
	theories/Overture.v
Merge branch 'upstream' into eqvar

Conflicts:
	theories/EquivalenceVarieties.v
	theories/Equivalences.v
	theories/Trunc.v
Reorder notations so Coq displays { & } rather than "exists"
Merge branch 'master' of https://github.com/spitters/HoTT into upstream

Conflicts:
	theories/EquivalenceVarieties.v
	theories/Equivalences.v
Fix naming inconsistency
shorten one proof, make 'idmap' an abbreviation
Starting to try S^1 as a private inductive type
a better proof of path_universe_inverse
comment out "Local" so it ought to compile without private types patch
finish the proof that pi1(S1)=Z
remove superfluous @s on transport
call it S1_rect
remove a superfluous eta-expansion
Simplify proof of S1_rectnd_beta_loop using apD_const
Move Circle.v to theories/hit directory