HoTT/HoTT — pull request #9 by andrejbauer (2012-03-18 17:23:27+00:00)
Title: Cleaned up circle examples, got rid of 8.2 compatibility.

I have included the proof that the circle is defined up to equivalence by its axioms.

I got rid of the supposed 8.2 compatibility which was not working anyhow.