HoTT/HoTT — pull request #67 by mikeshulman (2013-02-07 00:39:19+00:00)
Title: Hlevels

Changed HLevel to be a typeclass and fixed the numbering, propagating through all other proofs about h-levels in the library. I am noticing (as Bas said today) that it's important to be careful about what is added as an Instance; I added some comments about this in the code at a few places, and also in the STYLE file.