HoTT/HoTT — pull request #62 by mdnahas (2013-02-05 19:16:30+00:00)
Title: TypeClasses for Refl, Sym, Trans applied to Paths and Equiv.

The tactic "symmetry" was not working. We figured the better long term solution was to use a TypeClass for symmetry and just use "apply symmetry".

This commit declare a relation and 3 TypeClasses on it:
Reflexive
Symmetric
Transitive

Instances of all 3 exist for "paths" ("=") and "Equiv" ("<~>").

I changed "apply inverse" and "apply equiv_inverse" to "apply symmetry" where I found it.