Consistent use of symbol `•`: in `•-cong : Congruent₂ _•_` in `Algebra.Consequences.Setoid`

[jamesmckinna]

Is this the same symbol as discussed in #1544 ? If not, why not? And do we need to fix this?

Anywhere else that we might have 'identical' renderings of distinct symbols? cf #1544 on the potential for confusion...

[MatthewDaggitt]

Add entry to style guide describing how to type, and make one illegal.

[jamesmckinna]

Hmmm... it's not (all) quite what I previously believed/thought:

• Algebra.Consequences.Setoid does in fact seem to be locally-but-not-globally consistent, using \bu2 not \.
• but Algebra.Morphism.Consequences uses a different (but visually identical) symbol: \. inherited from Magma
• the \cdot of \cdot-cong fame, and Problems with change of Semilattice operation name #2166 , appears to be neither here nor there, it's 'just another different symbol'

So it seems that \. ought to be authoritative throughout for the first two, but not necessarily to be identified with the third?

UPDATED: I think that's squared away now by #2185 .

[jwaldmann]

Anywhere else that we might have 'identical' renderings of distinct symbols?

wat? never!

\top and T, :: and : negative-space : are totally not examples of that.

When these (or something very similar) were met with utter disbelief by beginners (including me) at an Agda tutorial, the speaker said "I know what you feel, and in my first year of using Agda, I tried to fight the unicode nonsense, but then gave up". Heeding the man's advice, I gave up from the start. I will however keep a bookmark to this issue here, under "temporarily confused library developer asks whether people would get temporarily confused by choice of symbols, but sanity gets restored, and issue is closed, promptly".

[MatthewDaggitt]

@jwaldmann , I closed this because the confusion complained about in this particular issue was closed by a PR. If you would like to open an issue to talk about more confusing instances or indeed general approaches to reducing confusion in general, then please do!

[jamesmckinna]

And as the "temporarily confused library developer" concerned, this issue/PR falls under "tidying up inconsistencies before a major release", where such inconsistencies inevitably arise over the course of the evolution of a large, long-lived, collaborative software project where not all such potential sources of inconsistency have been codified in a design, or style, document.

So to echo @MatthewDaggitt , please do file issue(s) if you are aware of other sources of inconsistency, or conventions you think it would be worth documenting or codifying...