agda-unimath
agda-unimath copied to clipboard
UniMath
Change symbol for similarity
The library has adopted the symbol ≈ for "similarity" of elements, for instance, for elements in preorders. However, it seems to me that the symbol ≈ is used more commonly to mean "approximates", e.g., "3 ≈ π" relative to some externally defined criterion. Part of the point of approximations is that they allow simplifying assumptions that include more solutions that are still satisfactory according to some criterion. However, with our current usage of the symbol, two elements are approximately the same in an extensional structure if and only if they are literally equal. Therefore, I propose using a different symbol for the notion of similarity of elements.
- Approximation at Wikipedia
- Almost equal to
≈at codepoints.net
Some suggestions for alternatives are
~, tilde, is already used for similarity of functions, and is commonly used for equivalence relation reasoning (note that approximation relations are commonly non-transitive!)∼, Tilde Operator (agda-input:\sim)≍, Equivalent To (agda-input:\asymp), is used for similarities/indistinguishabilities in the book The Univalence Principle
Out of the suggestions I'm most in favor of the last one, ≍, as it doesn't invoke associations with what the underlying structure is like (at least to me).
I don't have a better suggestion, but I really dislike the "Equivalent to" symbol, since it looks like the equals sign on all screens I have, unless I really zoom in.
I seem to remember seeing texts using ≈ to denote an arbitrary equivalence relation, so I'm not convinced the change is necessary. If we were to follow the unicode names or wikipedia tables of symbols, then we should also change our usage of tilde and simeq 😅
https://en.wikipedia.org/wiki/Similarity_(geometry) uses ~. (Also, the presumably LaTeX-inspired naming for \sim certainly seems suggestive.)
I'm a bit disappointed that you don't like the symbol ≍. In my experience it is just as distinct from = as ≈ and there seems to be at least some presedence in the literature for using ≍. I remember seeing it in another reference too, but I cannot remember which atm.
Oh and I forgot to say that I think my input should have minimal weight, since I rarely look at the modules where it's used anyway. But by the same token I wasn't sure if I should merge the PR