[mswphd]

I don't think quibbling over "equivalence" vs "equality" is useful personally. They're both "equality". Just what the sign "=" means differs depending on the type information.

E.g x: ZmodN == y: ZmodN is a different operation than x: Z == y: Z, but they're both the equality operation. We wouldn't makeup a new name for addition in this context.

It's also worth mentioning we can use the equality function (==): Z x Z -> bool to define the (==_N): ZmodN x ZmodN -> bool function in a semi-generic way. To do so, we "just" need a way to assign a unique representative (in Z) to any x: ZmodN. In other words, this is choosing a partial inverse to the reduction function modN: Z -> ZmodN. I think the partial inverse is a right inverse? so a function g : ZmodN -> Z such that (modN) o g x == x for all x in ZmodN. Anyway, given such a right inverse g, you can define (==_N): ZmodN x ZmodN -> bool via

(==_N) x y := (==) (g x) (g y)

This has the benefit that it doesn't treat ZmodN as special in any way. You can apply the same song and dance for more general quotient structures. This can be useful when doing e.g. matrix arithmetic, where you might want equivalence up to the choice of some rotation or something.