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
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
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
Commiting circle.v, but not really remembering what it was about
Starting to work on Yoneda lemma and colimits as HITs.

Initial transaltion of Egbert's Yoneda lemma and colimit
construction as Higher-Inductive type. WORK IN PROGRESS.
Modified the circle example so that we can have mutliple circles.

In order to prove that any two circles are the same we need to have
two circles to start with. But the standard axioms for the circle just
postulate one circle. So we change the axioms to a Coq Structure. Then
we may assume several instances of the structure.
Merging with upstream
Got rid of the fake 8.2 compatibility.

We used to "Unset Automatic Introduction, supposedly to be compatible
with Coq 8.2. However, this was not giving us any compatibility, as
there were other incompatibilities present. In any case, as Coq is now
already at 8.4 there is no point in keeping (fake) backward compatibility.
Moving experimental stuff to Experimental.