UniMath
font changes don't really work
Look at this:
I think using a font change to indicate application of a function is too cute, and likely to cause confusion.
Here I beg to differ. Using bold fonts to signify important constants has an enormous precedence even though it has some obvious disadvantages. Personally I'd prefer to use a simple bold (and not black board bold).
Bjorn
On 6 Aug 2021, at 16:33, Daniel R. Grayson @.***> wrote:
Look at this:
I think using a font change to indicate application of a function is too cute, and likely to cause confusion.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.
Well, for constants, it might be okay. But the example above is about the use for variables.
The problem with a simple bold is that it's a bit harder to tell apart from the regular weight.
@DanGrayson , what would you prefer instead as the notation for the canonical finite set with n elements? Fin n?
I think we should be pragmatic here. (Black board) Bold n is easy to read and only the most dogmatic of our readers will even think about it. If you feel strongly about it, we could under- or over line instead, but please stay clear of [n] and n_+.
Bjorn
On 9 Aug 2021, at 17:01, Ulrik Buchholtz @.***> wrote:
The problem with a simple bold is that it's a bit harder to tell apart from the regular weight.
@DanGrayson , what would you prefer instead as the notation for the canonical finite set with n elements? Fin n?
— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.
I'm not sure I understand the critic here. Is it about the differences between numerals and elements of N? In other words, do you mean that you would prefer having "For all numeral n, abbreviate \bn{n} [...]"?
If not, could you be more explicit about what is bothering you?
The problem is that the expression \bn n, as an expression, does not contain the variable n. Instead, it consists of a single variable, drawn from another alphabet. Expansion of definitions in an expression should not change which free variables appear in it.
And what about \bn m? Is it covered by this or not?
And what about
\bn m? Is it covered by this or not?
Yes, that's covered. But one case that isn't covered – and which we might need – is the case of a compound expression of type Nat. There we still need a way to map that to the corresponding canonical finite set.
And what about
\bn m? Is it covered by this or not?Yes, that's covered.
How is the student supposed to know it's covered?