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