> I think it's important to distinguish equality from equivalence. This is very true. In particular, equality ought to be merely a subset of equivalence. For c

> I think it's important to distinguish equality from equivalence. This is very true. In particular, equality ought to be merely a subset of equivalence. For codata types, as mentioned, equality may not be computable (or well-defined at all), but we can compute equivalences such as bisimulation if we like. For any type which has a nice equality then merely setting equivalence to equality should be fast, I agree. This is essentially `deriving Eq` in Haskell. Memberwise equality works for some types, but notably fails when we have abstraction. You can get away with it for (pure) functions on a finite domain if you really want but that's a little hacky---or rather, it involves (implicitly) injecting your function into some kind of container [0] and computing equality there. As you note, codata types aren't likely to have nice equalities. In these cases they're not going to have memberwise equality, either. [0] First chapter or so of these lecture notes if I remember correctly, http://lambda-the-ultimate.org/node/4804 http://lambda-the-ultimate.org/node/4804