The n-Category Café

Hi, It’s interesting that your syntax is fussy about non-symmetric props.

Sorry if I was too brief about monads. What I meant was this. Consider a colimit-preserving-monad $T$ on species. Every species is a colimit of representables, so to specify the action of $T$ on objects it suffices to specify the species $T(\mathbf{Bij}(n,-))$ for all $n$. In other words, $T$ is determined by the full subcategory $P$ of its Kleisli category spanned by the representables, together with the identity on objects inclusion functor $\mathbf{Bij}\to P$. In detail, the objects of $P$ are natural numbers, the morphisms $m\to n$ are natural transformations $\mathbf{Bij}(m,-)\to T(\mathbf{Bij}(n,-))$.

To make the monad $T$ commutative is to extend the monoidal structure of Species to the Kleisli category of $T$. The monoidal structure on representables satisfies $\mathbf{Bij}(m,-)\otimes \mathbf{Bij}(n,-)\cong\mathbf{Bij}(m+n,-)$. It follows that to make $T$ commutative is to give $P$ the structure of a prop.

The sifted colimit story is similar except we must use finite sums of representables instead of representables. For every species is a sifted colimit of a diagram of finite sums of representables.

You asked how our notations diverge. There’s two points, I think.

The first is that from my perspective the theories corresponding to props will always have a unique continuation. This is the point where I needed to generalize away from props. Quantum measurement is an example of something that has two possible continuations, depending on the classical outcome of the measurement. I’d say $\mathit{measure}:\neg(\mathit{qubit},\neg(),\neg())$. So $\mathit{measure}(a,t,u)$ measures qubit $a$ in the standard basis and continues as either $t$ or $u$ depending on the result. E.g. here is a quantum coin toss, that randomly continues as either $k$ or $l$:

where $\mathit{new}:\neg(\neg(\mathit{qubit}))$ supplies a new qubit initialized at $|0\rangle$, and and $H:\neg(\mathit{qubit},\neg(\mathit{qubit}))$ is the Hadamard rotation.

You could illustrate measurement like a string diagram for a prop but with the universe splitting in two, similar to how people illustrate possible worlds and also similar to how Paul-André Melliès illustrates local memory. I put a picture on page 2 of my paper (I’m not sure how to include it here). But I find these 3d diagrams hard to work with.

The second difference between our notations is what I called ‘commutativity’. Here I prefer your notation. Suppose $f:A\to C$ and $g:B\to D$. In your syntax you can compose them elegantly as $a:A,b:B\vdash (f(a),g(b)):C,D$. In my syntax there are two ways,

and if I wanted these to be equal I’d have to add an equation to impose this. To put it another way, the monads generated by my theories are always strong but not always commutative. This is fine for some purposes but it’s a hassle if you only want commutative theories.

I think I understand commutativity now, and I think I can see the multicategory-like notion corresponding to your sifted-colimit-preserving functors. But if I’m right, then I think there’s not much hope of a nice syntax generalizing my prop-type-theory to incorporate commutativity automatically in your case.

A commutative monad on a symmetric monoidal category $V$ is equivalently a commutative strong monoid object in the (virtual) symmetric duoidal category of endofunctors of $V$. If $V=[A^{op},Set]$ is a Day convolution structure with $A$ a small symmetric monoidal category, then the category of cocontinuous endofunctors is equivalent to $Prof(A,A)$ with a transferred duoidal structure, where $\star$ is profunctor composition and $\diamond$ is convolution with the monoidal structure $m:A\times A \to A$, i.e. $M\diamond N$ is the profunctor composite $A \xrightarrow{m^\ast} A\times A \xrightarrow{M\times N} A\times A \xrightarrow{m_\ast} A$.

A commutative strong monoid in a duoidal category is a $\star$-monoid with a compatible $\diamond$-module structure over the $\star$-unit $J$ (making it a “strong monoid”) satisfying a commutativity diagram. In $Prof(A,A)$ a $\star$-monoid is a bijective-on-objects functor $A\to B$. And $J$ is the identity profunctor, so a $J$-$\diamond$-module has the ability to “tensor morphisms of $B$ on by morphisms of $A$”, or equivalently with identities. Finally, the commutativity condition means that if we “tensor two morphisms of $B$” in the two possible ways, by first tensoring them with identities of $A$ and then composing, we get the same answer. Thus, we get a symmetric monoidal structure on $B$ making $A\to B$ a strict bijective-on-objects symmetric monoidal functor. (This is all in section 9.3 of arXiv:1507.08710.) Taking $A=Bij$ gives props.

If we relax cocontinuity to sifted-colimit-preservation, then instead of $Prof(A,A)$ we get $Prof(A,Prod(A))$ as mentioned above. The question is then what the transferred duoidal structure looks like. The $\star$-monoidal structure just comes from the structure of $Prod$, so it is the same as that going into the definition of cartesian multicategory; thus a $\star$-monoid consists of a bijective-on-objects functor from the underlying category of the monoidal category $A$ to the underlying category of a cartesian multicategory $B$. Since $Prod$ arose by dualization from $Coprod$ which gets its monoidal structure by restriction from the Day convolution, I believe that $\diamond$ is defined by the monoidal products in $A$ “distributing over” the cartesian products in $Prod$. Thus, a strong $\star$-monoid has the ability to tensor a morphism $f:(a_1,a_2,\dots,a_n) \to b$ of $B$ by an identity $1_c$ (or more generally a morphism of $A$) to get a morphism $f\otimes 1_c : (a_1\otimes c,a_2\otimes c,\dots,a_n\otimes c) \to b\otimes c$. Finally, commutativity means that if we “tensor two morphisms of $B$” in the two different ways, we get the same answer. If the morphisms are $f:(a_1,a_2,\dots,a_n) \to b$ and $g:(c_1,c_2,\dots,c_m) \to d$, then this equation becomes $$(1_b\otimes g) \circ (f\otimes 1_{c_1}, \dots, f\otimes 1_{c_m}) = (f\otimes 1_d) \circ (1_{a_1} \otimes g, \dots ,1_{a_n}\otimes g)$$ (modulo a rearrangement of the domains of both sides, in which the objects $a_i \otimes c_j$ appear in different orders).

The reason I say this seems unlikely to have a nice type theory is that the two morphisms being related contain the inputs $f$ and $g$ different numbers of times. For props, the commutativity relation is $(1_b\otimes g)\circ (f\otimes 1_c) = (f\otimes 1_d) \circ (1_a\otimes g)$, both sides of which contain $f$ and $g$ once each, so that we can expect a nice notation “$f\otimes g$” that means both of them. But in the sifted-colimit version above, the LHS contains one copy of $g$ and $m$ copies of $f$ while the RHS contains one copy of $f$ and $n$ copies of $g$. I can’t imagine how a term calculus could obtain the same thing by substituting $m$ copies of $f$ into a term containing one copy of $g$ as by substutiting $n$ copies of $g$ into a term containing one copy of $f$.