HoTT/HoTT — pull request #558 by mikeshulman (2014-10-07 17:30:25+00:00)
Title: eliminate :> in records and classes

I propose that we should not use the syntax `:>` in record and class definitions. I think it's confusing because sometimes it declares a coercion and sometimes an instance, and it's also a very small and easy-to-miss indicator for a very important thing to know about (a coercion). Instead I think it's better to give explicit `Coercion` and `Existing Instance` declarations.

Along the way I eliminated `equiv_isequiv` as a coercion, which doesn't make sense to me.