notations for 1 in category theory

Stream: maths

[Johan Commelin]

We have 1 all over maths.
In the category_lib we have \b1 for identity morphisms.
@Floris van Doorn has a PR that introduces bold-face 1 for functor.id.

Is this desirable? @Reid Barton @Scott Morrison any thoughts?
Random thought: would it be evil to give the functor category an instance of has_one? Then we could just reuse our familiar 1...

[Kevin Buzzard]

I usually use blackboard bold 1 for function 1

[Scott Morrison]

I think I had has_one for the functor category at some point, then removed it again. Unfortunately I don't remember why. Probably it was "don't have different names for the same thing --- you'll find yourself having to translate unnecessarily".

[Floris van Doorn]

It will probably be bad to make an identity morphism an instance of has_one: I expect that will require every has_one typeclass inference to run though all of the category instances, because maybe the current type is the type of morphisms in some category.

[Floris van Doorn]

For functor.id I don't think this is a problem (real does not unify with functor ?m ?m), so that might work. One potential problem is that we probably want to write 1 C : functor C C, with an explicit argument - which we probably cannot do with a has_one instance.

[Mario Carneiro]

I think that's the bigger issue - category 1 needs an explicit argument while regular 1 doesn't

[Floris van Doorn]

If that is the biggest issue, we could try making the functor.id argument implicit: often it can be inferred from context.

[Mario Carneiro]

My guess is this won't work in most cases, lean's elaborator isn't designed to handle this

[Mario Carneiro]

and also it's introducing another way to write id, which will need normalization to be useful

[Floris van Doorn]

My preference would be to have a global notation using some unicode 1. There are plenty of them, so it doesn't matter to much that the notation is global.

[Johan Commelin]

@Mario Carneiro Are you ok with making boldface 1 a global notation for functor.id?

[Mario Carneiro]

isn't it already?

[Johan Commelin]

No, it's not yet

[Mario Carneiro]

well there's double struck 1, is that global?

[Johan Commelin]

Floris is introducing it in a current PR, hence this discussion

[Mario Carneiro]

does that work as functor.id?

[Johan Commelin]

Yes, that's for id-morphisms

[Johan Commelin]

Nope, it doesn't because functors aren't morphisms atm

[Mario Carneiro]

it seems similar to the question of eliminating the nat-trans arrow

[Johan Commelin]

We could build CAT as a 1-category... but that also seems like a hack

[Johan Commelin]

Also, it means that we have to bundle categories... so it actually doesn't work

[Johan Commelin]

@Mario Carneiro Does that justify the introduction of new notation?

[Mario Carneiro]

Is there a vscode abbreviation for bold 1?

[Johan Commelin]

Not yet

[Mario Carneiro]

then go for it

[Johan Commelin]

@Floris van Doorn :up:

[Mario Carneiro]

if all else fails you can use emoji 1

[Mario Carneiro]

Personally I prefer variegated ascii sentinels but you mathematicians like your high unicode

[Johan Commelin]

It's just that I'm a bit worried where this will end...

[Mario Carneiro]

which one? Unicode crazy or ASCII crazy

[Mario Carneiro]

or just long names

[Johan Commelin]

Notation crazy

[Johan Commelin]

We write $\mathrm{id}_C$ and get on with life

[Johan Commelin]

Our brains use the type of $C$ to figure out the rest

[Johan Commelin]

Oooh, that's not true

[Mario Carneiro]

What's wrong with 1F?

[Johan Commelin]

We use the type of $C$ plus all available "type class instances"

[Mario Carneiro]

the problem with bold vs double struck is you can't tell which is which

[Johan Commelin]

And whether you can figure those out is part of what makes you a "knowledgeable reader"

[Mario Carneiro]

and I usually get the sense from the mathematician that "yes that's the point, I want them to be indistinguishable"

[Mario Carneiro]

but of course in real use it matters which is which

[Johan Commelin]

They should only be indistinguishable if they really are... I.e. if you type the same thing into VScode

[Johan Commelin]

Otherwise users have to start remembering the differences... and in that case the difference better be self-explanatory

[Johan Commelin]

So that is maybe an argument in favor of 1F

[Johan Commelin]

Or maybe \b1 F

[Mario Carneiro]

they need to be attached to make it one symbol

[Johan Commelin]

Sure

[Mario Carneiro]

using fancy unicode at that point serves no purpose

[Johan Commelin]

But I wanted to indicate that it wasn't 1 VScode slash-code

[Johan Commelin]

It does... it shows that it's related to ordinary \b1

[Mario Carneiro]

oh, is \b1 the double struck one?

[Mario Carneiro]

that's not confusing at all

[Reid Barton]

So, do we have a suggested way to enter the bold 1 in vscode/emacs?