@amiloradovsky@functional.cafe I think the first one might be closest to what people usually mean by equality (not that I understand at all what is said, but I like the word "literally"). I would describe it as equivalence relation that always holds, no matter the context (for certain meaningful set of contexts you are dealing with). The others are looser and are usually called equivalence even in rather informal setting. In one way or the other you need to keep track of these contextual relations, as they can confuse the intuition just as well. The symbol is overloaded to reuse formulas, so I imagine it can't be very useful when trying to define everything in a "global" context.