Inconsistent usage of "·" and "∙"

[VojtechStep]

The first middle-dot is · ("MIDDLE DOT", codepoint #xb7), and it's used in left and right whiskering (_·l_ and _·r_ in foundation-core.homotopies).
The other one is ∙ ("BULLET OPERATOR", codepoint #x2219), and it's used in the same file for homotopy concatenation, just a few lines above left and right whiskering.

To my knowledge, the middle dot can't even be typed using agda-input.

From a cursory look through the output of greping for MIDDLE DOT, it's only used for these two whiskering operators and some prose in groups and rings. Perhaps these occurences should be replaced by the other symbol?

[fredrik-bakke]

Are you unable to type this symbol using the sequence cdot or centerdot?

[fredrik-bakke]

To my understanding, the difference in symbol usage is precisely to contrast whiskering from homotopy concatenation.

[VojtechStep]

Are you unable to type this symbol using the sequence cdot?

I'm not at my computer anymore, but I tried looking through all the symbols I could type with \., and this wasn't one of them, C-u C-x = told me that I could only write it with C-x 8 RET, and I tried searching in agda-input.el, but it wasn't there; though now I see that Agda input inherits from TeX, so it's completely possible that I just didn't try hard enough.

And if the distinction is intentional, then maybe it could be written down somewhere? I'm not sure if it's the font I use (JetBrains Mono), or my Emacs configuration, but these two symbols look identical to me (I now see that they have different size on my phone).

[fredrik-bakke]

Well, that's definitively an issue; these symbols should not look the same. I would suggest changing your font.
The website uses the following series of fonts in prioritized order (decreasing) to display agda code:

font-family: Menlo, Source Code Pro, Consolas, Monaco, Lucida Console, Liberation Mono, DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New, monospace, serif;

so you can try one of these.

The documentation can definitely be added; this is an unfortunate experience to have.

[fredrik-bakke]

I have created pull request #465 to address this issue. Please take a look, and feel free to suggest further changes that can help mitigate this.

[VojtechStep]

The website uses the following series of fonts in prioritized order (decreasing) to display agda code:

font-family: Menlo, Source Code Pro, Consolas, Monaco, Lucida Console, Liberation Mono, DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New, monospace, serif;

so you can try one of these.

Actually the two symbols look the same for me even on the website, see the attached screenshots. I'll check how it looks on my computer later in the afternoon.

I checked how the two symbols look in various contexts, and these are my results:

• My editor: indistinguishable (JetBrains Mono), I don't have a screenshot at the moment
• Website on mobile: indistinguishable (not sure which font is picked) [1][2]
• GitHub website on mobile: barely distinguishable, I suspect that's mostly the work of different padding around the dots inside the quotation marks [3]
• GitHub application on mobile: indistinguishable [4]
• Discord bot message: clear difference [5]

1
2
3
4
5

[fredrik-bakke]

Thank you for the additional information!
I am guessing this is due to your devices not having the most prioritized fonts installed, and whichever one they are falling back to is not good. Hopefully, this can be improved if we change our font prioritization on the website. I don't think we should worry about how it displays in the issue header, as it is not designed to display code that way, although your screenshots are demonstrative.

[VojtechStep]

I tried to find out how the different fonts used for the website show the two symbols, and this is what I found (I think some of the fonts don't support the characters, in which case the browser probably chooses a fallback font):

• Menlo: no information, I don't own any Apple products
• Source Code Pro: indistinguishable [1]
• Consolas: indistinguishable [2]
• Monaco: indistinguishable [3]
• Lucida Console: distinct, bullet is a non-centered square [4]
• Liberation Mono: indistinguishable [5]
• DejaVu Sans Mono: distinct, bullet is a square [6]
• Bitstream Vera Sans Mono: indistinguishable [7]
• Courier New OS: distinct, but I would need to see them side-by-side [8]

source: fontmirror, fonts.com

I think having these two symbols be almost identical is more frequent then not. If I'm looking at the website's source correctly, it ships a copy of Source Code Pro; it would make sense to me to distribute also a font which distinguishes the two dots - from this list, that would be Lucida Console (but AFAIK that one needs a license, so that's a problem), or DejaVu Sans Mono (which should be redistributable).

1

2

3

4

5

6

7

8

[fredrik-bakke]

I agree with this. Another option would also be to redistribute Courier New.

[fredrik-bakke]

@jonaprieto Do you know how to fix this?

[fredrik-bakke]

For reference, here's how the symbols are displayed in my Brave browser on a mac.

In agda code:


Looks like perhaps Deja Vu Mono is used here.

In non-agda code:

As an extension of this issue, it would make sense if the same font was used in both of these scenarios.