benediktahrens/HoTT — pull request #1 by JasonGross (2014-05-07 13:20:20+00:00)
Title: Fix typeclass problems so that most of precategories compile

There was already a definition of `hSet` and appropriate instances around that. For the rest of the library, I suspect that the primary change to make is to replace `Definition` or `Lemma` with `Instance` whenever you are proving an `isaset` or `isaprop` goal. When Coq won't let you apply a lemma, you can do `apply @lem` (instead of `apply lem`) to get it to not try to resolve typeclasses.