> This leads to the deeply weird situation where "⩵" ≠ "==" and absolutely no programming language that I know of will let you use the correct Unicode character

> This leads to the deeply weird situation where "⩵" ≠ "==" and absolutely no programming language that I know of will let you use the correct Unicode characters! What about Agda? I was impressed how Agda allows you to use a lot of Unicode operators and ascii character sequences to do the same thing (e.g. → and `->`). Not sure about the situation he mentions above, but I'd bet Agda supports it too.