Comment by auggierose

> In traditional mathematics equality is treated as a relation. Two things are either equal or not.

That sounds like the way to go. No (identity) types needed.