## Stream: maths

### Topic: binary (co)products notation

#### 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.

#### Scott Morrison (Sep 06 2019 at 23:42):

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

#### 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.

#### Scott Morrison (Sep 08 2019 at 04:24):

Shall I just PR these?

Done as #1413.

#### Reid Barton (Sep 08 2019 at 10:07):

I do agree the ' looks a bit nicer

#### Reid Barton (Sep 08 2019 at 10:07):

What do you mean about a subscript?

#### 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.

#### 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.

ah, I see

#### Scott Morrison (Sep 08 2019 at 10:26):

So, ' or _ here?

#### 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. :-)

#### 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?

#### Reid Barton (Sep 11 2019 at 12:33):

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

#### Scott Morrison (Sep 11 2019 at 21:35):

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

#### 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"

#### Reid Barton (Sep 11 2019 at 21:45):

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

#### Scott Morrison (Sep 11 2019 at 21:55):

Okay, I've updated the PR.

#### Scott Morrison (Sep 11 2019 at 21:55):

We also need to add shortcuts in VSCode

#### Scott Morrison (Sep 11 2019 at 21:56):

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

#### Johan Commelin (Sep 12 2019 at 06:02):

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

#### Scott Morrison (Sep 12 2019 at 06:08):

Sounds good to me. What about ⨿?

#### Scott Morrison (Sep 12 2019 at 06:08):

\UU??

#### Johan Commelin (Sep 12 2019 at 06:09):

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

#### 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