Started working on theorems which show that definable types have good properties w.r.t. equivalence and univalence
Merge branch 'master' of github.com:HoTT/HoTT
Changed notation for equivalence to ~=>, which I don't particularly like, because LaTeX choked on it.
Changed notation for inverses to ASCCI "inv w" because LaTeX choked on it
Changed notation for extensional equality of functions to == because LaTeX choked on it
Removed "Unset Automatic Introduction." and thus departed from Coq 8.2 compatibility.
Working on definable extensionality
Changed Makefile to avoid constant recompilation of all files
Merge branch 'master' of github.com:HoTT/HoTT
Commiting before merge
Merge github.com:HoTT/HoTT

Conflicts:
	Coq/Contractible.v
	Coq/Equivalences.v
	Coq/FiberEquivalences.v
	Coq/Fibrations.v
	Coq/Funext.v
	Coq/HLevel.v
	Coq/Paths.v
	Coq/Univalence.v
	Coq/UnivalenceImpliesFunext.v
Update HIT/Makefile also to avoid constant recompilation.
Removed dependency of .v files on .depend
Trying to improve Circle.v, does not compile at the moment
testing github
Converted Circle to a structure. Borrowed the proof that any two
circles are equivalent from Guillaume Brunerie, and adapted it so
that it actually works with two circles.
Improved cc_transp lemma in CircleWellDefined.v
Merge pull request #5 from mikeshulman/forupstream

Update HIT/Makefile also to avoid constant recompilation.
Ignore .v.d's
Adding inductive types in HoTT.