Zulip Chat Archive

Stream: maths

Topic: binary (co)products notation


view this post on Zulip Reid Barton (Sep 06 2019 at 14:55):

We seem to be taking over notation ending in _ in category theory; maybe we should use ×_ for product then?
By the way, I'm not sure how I feel about using the symbol for the coproduct. ⨿ seems more appropriate if we can use it.

view this post on Zulip Scott Morrison (Sep 06 2019 at 23:42):

Both suggestions seem pretty reasonable. Perhaps we should reserve for biproducts?

view this post on Zulip Scott Morrison (Sep 08 2019 at 04:24):

By the way --- my initial use of these "terminal _" notations was all in places where common maths notation used a subscript. These ⨿_ and ×_ notations are fine, but much less readable than the original uses.

view this post on Zulip Scott Morrison (Sep 08 2019 at 04:24):

Shall I just PR these?

view this post on Zulip Scott Morrison (Sep 08 2019 at 05:16):

Done as #1413.

view this post on Zulip Reid Barton (Sep 08 2019 at 10:07):

I do agree the ' looks a bit nicer

view this post on Zulip Reid Barton (Sep 08 2019 at 10:07):

What do you mean about a subscript?

view this post on Zulip Scott Morrison (Sep 08 2019 at 10:12):

I think the first place I introduced notations with a trailing _ was in the monoidal categories definition:

notation `𝟙_` := tensor_unit
notation `α_` := associator
notation `λ_` := left_unitor
notation `ρ_` := right_unitor

So you can write for example λ_ X, which reads very naturally to me as "lambda-subscript-X", which is exactly what you'd usually see for the component of a natural transformation.

view this post on Zulip Scott Morrison (Sep 08 2019 at 10:13):

That is, I was using the trailing subscript in places where it was natural to expect a subscript.

view this post on Zulip Reid Barton (Sep 08 2019 at 10:14):

ah, I see

view this post on Zulip Scott Morrison (Sep 08 2019 at 10:26):

So, ' or _ here?

view this post on Zulip Scott Morrison (Sep 08 2019 at 10:26):

Personally, I'm not that keen on notations at all, so I find it a bit hard to care which. :-)

view this post on Zulip Reid Barton (Sep 11 2019 at 12:33):

Or we could be more creative; how about ⨯? In my font it looks like a bigger × and it's \X in emacs. Not really semantically sensible according to its Unicode name (VECTOR OR CROSS PRODUCT) but maybe that doesn't matter?

view this post on Zulip Reid Barton (Sep 11 2019 at 12:33):

Likewise, we don't really need a prime or anything on ⨿

view this post on Zulip Scott Morrison (Sep 11 2019 at 21:35):

In my font it looks pretty similar to the normal \times. I'm game, though.

view this post on Zulip Reid Barton (Sep 11 2019 at 21:44):

Hopefully it should not be too confusing if they look similar, since if both make sense they should be "the same"

view this post on Zulip Reid Barton (Sep 11 2019 at 21:45):

... assuming that the category-theory product of types is the actual prod product

view this post on Zulip Scott Morrison (Sep 11 2019 at 21:55):

Okay, I've updated the PR.

view this post on Zulip Scott Morrison (Sep 11 2019 at 21:55):

We also need to add shortcuts in VSCode

view this post on Zulip Scott Morrison (Sep 11 2019 at 21:56):

Any suggestions? \X is already taken in VSCode for Ξ

view this post on Zulip Johan Commelin (Sep 12 2019 at 06:02):

I wouldn't mind stealing \X, and turning the existing on into \Xi.

view this post on Zulip Scott Morrison (Sep 12 2019 at 06:08):

Sounds good to me. What about ⨿?

view this post on Zulip Scott Morrison (Sep 12 2019 at 06:08):

\UU??

view this post on Zulip Johan Commelin (Sep 12 2019 at 06:09):

Sure, and maybe also \coprod because I'll forget the other

view this post on Zulip Patrick Massot (Sep 12 2019 at 20:04):

Is this cross the one I used to use and @Edward Ayers accidentally removed? If yes then I'm all in favor of restoring it in the VScode translation file, but please make that a local notation in the category theory library


Last updated: May 12 2021 at 08:14 UTC