## Stream: maths

### Topic: notations for 1 in category theory

#### Johan Commelin (May 06 2019 at 16:08):

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 (May 06 2019 at 16:08):

I usually use blackboard bold 1 for function 1

#### Scott Morrison (May 06 2019 at 19:29):

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 (May 07 2019 at 00:44):

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 (May 07 2019 at 00:45):

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 (May 07 2019 at 00:46):

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

#### Floris van Doorn (May 07 2019 at 00:50):

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

#### Mario Carneiro (May 07 2019 at 00:51):

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

#### Mario Carneiro (May 07 2019 at 00:51):

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

#### Floris van Doorn (May 07 2019 at 00:56):

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 (May 07 2019 at 03:27):

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

No, it's not yet

#### Mario Carneiro (May 07 2019 at 03:27):

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

#### Johan Commelin (May 07 2019 at 03:27):

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

#### Mario Carneiro (May 07 2019 at 03:28):

does that work as functor.id?

#### Johan Commelin (May 07 2019 at 03:28):

Yes, that's for id-morphisms

#### Johan Commelin (May 07 2019 at 03:28):

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

#### Mario Carneiro (May 07 2019 at 03:28):

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

#### Johan Commelin (May 07 2019 at 03:28):

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

#### Johan Commelin (May 07 2019 at 03:29):

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

#### Johan Commelin (May 07 2019 at 03:41):

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

#### Mario Carneiro (May 07 2019 at 03:42):

Is there a vscode abbreviation for bold 1?

Not yet

then go for it

#### Johan Commelin (May 07 2019 at 03:43):

@Floris van Doorn :up:

#### Mario Carneiro (May 07 2019 at 03:43):

if all else fails you can use emoji 1

#### Mario Carneiro (May 07 2019 at 03:44):

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

#### Johan Commelin (May 07 2019 at 03:46):

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

#### Mario Carneiro (May 07 2019 at 03:47):

which one? Unicode crazy or ASCII crazy

#### Mario Carneiro (May 07 2019 at 03:47):

or just long names

Notation crazy

#### Johan Commelin (May 07 2019 at 03:47):

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

#### Johan Commelin (May 07 2019 at 03:48):

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

#### Johan Commelin (May 07 2019 at 03:48):

Oooh, that's not true

#### Mario Carneiro (May 07 2019 at 03:48):

What's wrong with 1F?

#### Johan Commelin (May 07 2019 at 03:48):

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

#### Mario Carneiro (May 07 2019 at 03:48):

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

#### Johan Commelin (May 07 2019 at 03:49):

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

#### Mario Carneiro (May 07 2019 at 03:49):

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

#### Mario Carneiro (May 07 2019 at 03:49):

but of course in real use it matters which is which

#### Johan Commelin (May 07 2019 at 03:49):

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

#### Johan Commelin (May 07 2019 at 03:50):

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

#### Johan Commelin (May 07 2019 at 03:50):

So that is maybe an argument in favor of 1F

#### Johan Commelin (May 07 2019 at 03:50):

Or maybe \b1 F

#### Mario Carneiro (May 07 2019 at 03:51):

they need to be attached to make it one symbol

Sure

#### Mario Carneiro (May 07 2019 at 03:51):

using fancy unicode at that point serves no purpose

#### Johan Commelin (May 07 2019 at 03:51):

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

#### Johan Commelin (May 07 2019 at 03:52):

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

#### Mario Carneiro (May 07 2019 at 03:52):

oh, is \b1 the double struck one?

#### Mario Carneiro (May 07 2019 at 03:52):

that's not confusing at all

#### Reid Barton (May 10 2019 at 22:43):

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

Last updated: May 12 2021 at 08:14 UTC