Update STYLE, incorporating wiki; close #468

I don't know; does anyone remember the reason for that decision?  One might argue that since `foo` in `foo ^-1` is a function that happens to be an equivalence, rather than an `Equiv` object, so should `foo ^-1` be.  But it is somewhat annoying to have to write `equiv_inverse` when that's what we mean, and given `equiv_fun` as a coercion, maybe it wouldn't be a problem for `^-1` to mean `equiv_inverse`?