Semigroupoidal category

Stream: Is there code for X?

[Yaël Dillies]

A monoidal category has an associator, a left unitor and a right unitor. But now I have the category Twop which has just an associator. How should I go about it? Should we have semigroupoidal categories in mathlib or should I define the tensor product ad hoc and provide its properties by hand?

[Adam Topaz]

How did you define Twop? Twop means two distinct points?

[Adam Topaz]

If you work with two possibly equal points, then it should just be monoidal right? So you could construct both categories and consider the monoidal structure in the actual monoidal category

[Kevin Buzzard]

I see -- so a bipointed set is different to a two-pointed set!

[Adam Topaz]

This is like considering the category of rings where $1 \neq 0$ as opposed to the usual category of rings. Who does that?!

[Reid Barton]

Another place this comes up is sSet as the classifying topos for linear orders with $\bot \ne \top$

[Reid Barton]

I think there is some more standard terminology for this "equipped with two distinct (but labeled) points" but I forget what it is

[Kyle Miller]

(In case you ever remember what that terminology is, here's a link to the relevant poll.)

[Damiano Testa]

These are like configuration spaces right?

[Adam Topaz]

It's related -- a point in $\operatorname{Conf}_2(X)$ corresponds to a 2-pointed structure on $X$ (with the points distinct). But what Yael is considering is the category of all triples $(X,a,b)$ with $X$ a set, $a,b \in X$ and $a \neq b$ (with the natural category structure, where morphisms are functions on the set which send $a$ to $a$ and $b$ to $b$).

[Yaël Dillies]

(I'm actually not sure about the sends $a$ to $a$ and $b$ to $b$ part. The nLab page is unclear to me on that point)

[Yaël Dillies]

I can define Bipointed and work over that, but won't I need to restrict to Twop at some point?

[Yaël Dillies]

Also, Bhavik explicitly told me not to define Bipointed :stuck_out_tongue:

[Kevin Buzzard]

Bipointed is the kind of stack which shows up in algebraic geometry -- we're into our moduli stacks and these are simple examples

[Yaël Dillies]

/me is defining Bipointed

[Bhavik Mehta]

Yaël Dillies said:

Also, Bhavik explicitly told me not to define Bipointed :stuck_out_tongue:

I thought I said not to define it unless you need it! But now it seems like you need it :)