some more hints for working with typeclasses
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.
Added notation [g o f] for composition.
Merge pull request #84 from mikeshulman/eqvar

Comparing notions of equivalence (with some other minor changes)
Merge branch 'master' of https://github.com/HoTT/HoTT
improve proof of isprop_biinv
Incorporated [g o f] notation into EquivalenceVarieties.
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