Zulip Chat Archive

Stream: maths

Topic: notations for 1 in category theory


view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (May 06 2019 at 16:08):

I usually use blackboard bold 1 for function 1

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 07 2019 at 03:27):

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

view this post on Zulip Mario Carneiro (May 07 2019 at 03:27):

isn't it already?

view this post on Zulip Johan Commelin (May 07 2019 at 03:27):

No, it's not yet

view this post on Zulip Mario Carneiro (May 07 2019 at 03:27):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:27):

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

view this post on Zulip Mario Carneiro (May 07 2019 at 03:28):

does that work as functor.id?

view this post on Zulip Johan Commelin (May 07 2019 at 03:28):

Yes, that's for id-morphisms

view this post on Zulip Johan Commelin (May 07 2019 at 03:28):

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

view this post on Zulip Mario Carneiro (May 07 2019 at 03:28):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:28):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:29):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:41):

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

view this post on Zulip Mario Carneiro (May 07 2019 at 03:42):

Is there a vscode abbreviation for bold 1?

view this post on Zulip Johan Commelin (May 07 2019 at 03:42):

Not yet

view this post on Zulip Mario Carneiro (May 07 2019 at 03:42):

then go for it

view this post on Zulip Johan Commelin (May 07 2019 at 03:43):

@Floris van Doorn :up:

view this post on Zulip Mario Carneiro (May 07 2019 at 03:43):

if all else fails you can use emoji 1

view this post on Zulip Mario Carneiro (May 07 2019 at 03:44):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:46):

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

view this post on Zulip Mario Carneiro (May 07 2019 at 03:47):

which one? Unicode crazy or ASCII crazy

view this post on Zulip Mario Carneiro (May 07 2019 at 03:47):

or just long names

view this post on Zulip Johan Commelin (May 07 2019 at 03:47):

Notation crazy

view this post on Zulip Johan Commelin (May 07 2019 at 03:47):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:48):

Our brains use the type of CC to figure out the rest

view this post on Zulip Johan Commelin (May 07 2019 at 03:48):

Oooh, that's not true

view this post on Zulip Mario Carneiro (May 07 2019 at 03:48):

What's wrong with 1F?

view this post on Zulip Johan Commelin (May 07 2019 at 03:48):

We use the type of CC plus all available "type class instances"

view this post on Zulip Mario Carneiro (May 07 2019 at 03:48):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:49):

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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (May 07 2019 at 03:49):

but of course in real use it matters which is which

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 07 2019 at 03:50):

So that is maybe an argument in favor of 1F

view this post on Zulip Johan Commelin (May 07 2019 at 03:50):

Or maybe \b1 F

view this post on Zulip Mario Carneiro (May 07 2019 at 03:51):

they need to be attached to make it one symbol

view this post on Zulip Johan Commelin (May 07 2019 at 03:51):

Sure

view this post on Zulip Mario Carneiro (May 07 2019 at 03:51):

using fancy unicode at that point serves no purpose

view this post on Zulip Johan Commelin (May 07 2019 at 03:51):

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

view this post on Zulip Johan Commelin (May 07 2019 at 03:52):

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

view this post on Zulip Mario Carneiro (May 07 2019 at 03:52):

oh, is \b1 the double struck one?

view this post on Zulip Mario Carneiro (May 07 2019 at 03:52):

that's not confusing at all

view this post on Zulip 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