HoTT/HoTT — pull request #337 by JasonGross (2014-03-10 12:12:40+00:00)
Title: 2 sphere direct

Do we want a direct definition of the 2-sphere as a HIT, as in the book?