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.