Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
A definition (perhaps novel but obvious) that works in a cartesian multicategory
I’m very curious if it’s possible to define a similar version of traced monoidal category that works in an arbitrary (symmetric?) multicategory.
Correction: we know a fixed point operator on a Lawvere theory is the same thing as a Conway theory. (Hmm. Maybe Max, your fixed point operator for a one-object cartesian multicategory isn’t the same as a fixed point operator on the corresponding Lawvere theory regarded as a category with products. i.e. maybe a fixed point operator on a cartesian multicategory isn’t as strong as a fixed point operator on the corresponding cartesian category. Unsure about how to deal with mutually recursive definitions. Didn’t think about it for very long though and may have missed a trick.)
I missed that page, these should probably be merged into one.
As to mutual vs single fixed points, it’s a good question. The definition I took is from Simpson and Plotkin and I simply noticed that the definition made sense in an arbitrary cartesian multicategory. What I overlooked though is that of course because they were working with a cartesian category, they were really defining all mutual fixed points as well, so my definition isn’t clearly equivalent to theirs.
However, I thought mutual fixed points wouldn’t be needed, because (1) you can define them by Bekič’s construction, and (2) Simpson and Plotkin show that in a cartesian category the version of the axioms I gave satisfies “Bekič’s property”, i.e., that a fixed point of a product can be defined as a nested fixed point.
I have a sketch on the board that this proof works for my multicategory axioms, so if the multicategory is representable, then a fixed point of a product is equal to a nested fixed point. I’ll need to think to figure out whether or not I can extend that argument to the equivalence with Conway operators.
Update: I looked at this morning and it got a little too gnarly for me. If we call my definition a multi-FPO, then I am fairly convinced that multi-FPO on a representable cartesian multicategory is equivalent to trace on as a cartesian monoidal category.
What I am not totally convinced of is that a multi-FPO on is the same thing as a (multi-sorted) Conway operator, which is equivalent to a trace on . Maybe there’s some abstract argument (I pray) but I don’t see one. You can define the data of a Conway operator by induction on the length of the context, but the equations for dinaturality/diagonal lemma got too gnarly for me to justify figuring out when I don’t have a strong reason.
1 to 9 of 9