julesh on Nostr: npub1ky223…rghvc The example there is unbelievably cursed, I previously believed ...
npub1ky223zcc4q69d8t0me4vg5uw8mw0yxeukjgvz6h92laqnenr0ajs5rghvc (npub1ky2…ghvc) The example there is unbelievably cursed, I previously believed this couldn't happen
I don’t think this issue affects string diagrams in theory, it happens "upstream” at the point where you turn a finite product category into a cartesian monoidal category. A string diagram can be semantically interpreted in any monoidal category, and the data of a monoidal category includes a choice of unitors. What this tells us is that “the semantics of.a string diagram in a finite product category" may not be well defined, which to me is surprising, but doesn't contradict the proven coherence theorems
(I already had my suspicions that proving "every finite product category is cartesian monoidal” in general requires large amounts of axiom of choice, which if true is a less serious issue in the same place)
I don’t think this issue affects string diagrams in theory, it happens "upstream” at the point where you turn a finite product category into a cartesian monoidal category. A string diagram can be semantically interpreted in any monoidal category, and the data of a monoidal category includes a choice of unitors. What this tells us is that “the semantics of.a string diagram in a finite product category" may not be well defined, which to me is surprising, but doesn't contradict the proven coherence theorems
(I already had my suspicions that proving "every finite product category is cartesian monoidal” in general requires large amounts of axiom of choice, which if true is a less serious issue in the same place)