binary (co)products notation

Stream: maths

[Reid Barton]

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]

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

[Scott Morrison]

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]

Shall I just PR these?

[Scott Morrison]

Done as #1413.

[Reid Barton]

I do agree the ' looks a bit nicer

[Reid Barton]

What do you mean about a subscript?

[Scott Morrison]

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]

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

[Reid Barton]

ah, I see

[Scott Morrison]

So, ' or _ here?

[Scott Morrison]

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

[Reid Barton]

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]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

Okay, I've updated the PR.

[Scott Morrison]

We also need to add shortcuts in VSCode

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

Sounds good to me. What about ⨿?

[Scott Morrison]

\UU??

[Johan Commelin]

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

[Patrick Massot]

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