July 10, 2014

Describing PROPs Using Generators and Relations

Posted by John Baez Here’s another post asking for a reference to stuff that should be standard. (The last ones succeeded wonderfully, so thanks!)

I should be able to say

$C$ is the symmetric monoidal category with the following presentation: it’s generated by objects $x$ and $y$ and morphisms $L: x \otimes y \to y$ and $R: y \otimes x \to y$, with the relation

$(L \otimes 1)(1 \otimes R)\alpha_{x,y,x} = (1 \otimes R)(L \otimes 1)$

Here $\alpha$ is the associator. Don’t worry about the specific example: I’m just talking about a presentation of a symmetric monoidal category using generators and relations.

Right now Jason Erbele and I have proved that a certain symmetric monoidal category has a certain presentation. I defined what this meant myself. But this has got to be standard, right?

So whom do we cite?

You are likely to mention PROPs, and that’s okay if they get the job done. But I don’t actually know a reference on describing PROPs by generators and relations. Furthermore, our actual example is not a strict symmetric monoidal category. It’s equivalent to one, of course, but it would be nice to have a concept of `presentation’ that specified the symmetric monoidal category only up to equivalence, not isomorphism. In other words, this is a ultimately a 2-categorical concept, not a 1-categorical one.

If it weren’t for this, we could use the fact that PROPs are models of an algebraic theory. But our paper is actually about control theory—a branch of engineering—so I’d rather avoid showing off, if possible.

Posted at July 10, 2014 11:34 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2752

Re: Describing PROPs Using Generators and Relations

Well, (non-strict) symmetric monoidal categories are the (strict) algebras for a 2-monad. So you could use the standard notion of “generators and relations” for algebras over a monad, i.e. a coequalizer of maps between free algebras. That would specify it up to isomorphism, though.

Your example suggests that maybe you’re thinking instead of a codescent object of maps between free algebras, where you would give generating objects, generating morphisms, and relations on the morphisms. Codescent objects (unlike coequalizers) are flexible colimits, so there the strict colimit is equivalent to the bicategorical one, and the latter is specified only up to isomorphism.

Posted by: Mike Shulman on July 10, 2014 6:20 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

My thoughts were the same as those in Mike’s first paragraph. I guess I’d be a little bit surprised if anyone had written specifically about generators and relations for PROPs.

As regards what to cite, maybe Blackwell, Kelly and Power’s 1989 paper “Two-dimensional monad theory”. It’s a time-honoured tradition to cite that paper whenever saying anything whatsoever about 2-monads.

Posted by: Tom Leinster on July 11, 2014 10:02 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

You guys are a bit too smart; you’d have me derive the necessary results for PROPs myself, starting from some more general theory. I admit to some attraction to doing this: we’d then have the first paper on control theory that used 2-monads. And if I need to do it, I will.

But there’s a humble tradition of citizens using PROPs for all sorts of practical chores. These people sometimes describe PROPs using generators and relations. It is, after all, one of the main ways to describe PROPs! It’s just like how in practice you often give an algebraic theory by giving a sketch.

Here’s an example:

You’ll see a bunch of definitions like

Definition 2. The PROP for commutative monoids is freely generated by morphisms $i : 1 \to x$, $m : x \otimes x \to x$ obeying equations…

and leading up to ones that are much more novel and interesting, like the PROP for interacting Hopf algebras. They know plenty of category theory—they use Steve Lack’s work on distributive laws for PROPs, for example. And they act like everyone knows what it means to specify a PROP by generators and relations. So I’m wondering who, if anyone, has discussed this.

Maybe everyone just thinks its too obvious. And if you think of PROPs as algebraic structures akin to groups and rings, it sort of is. But when you drift into thinking of them as ‘2-algebraic’, specified up to equivalence rather than isomorphism, it seems worth at least a page of discussion somewhere.

Mike wrote:

Codescent objects (unlike coequalizers) are flexible colimits, so there the strict colimit is equivalent to the bicategorical one, and the latter is specified only up to isomorphism.

Did you mean only up to equivalence?

Posted by: John Baez on July 12, 2014 7:47 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Did you mean only up to equivalence?

Yes, sorry.

And they act like everyone knows what it means to specify a PROP by generators and relations.

Well, then, it sounds like they know the answer. Maybe you should ask them! (-: You could also ask (or try to guess from the paper — I haven’t looked at it) whether they ever think of PROPs as “2-algebraic”, or only “1-algebraic”.

Posted by: Mike Shulman on July 12, 2014 8:33 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

It’s not that I think it’s “too obvious”, or even that I know 2-monad theory very well (I don’t). It’s simply that I don’t know a direct reference for generators and relations of PROPs. If I did, then of course I wouldn’t have been shy about mentioning it. The 2-monad reference was the best I could do.

Come to think of it, I don’t know a reference for plain old categories presented by generators and relations. One often sees on-the-fly definitions such as:

Let $\mathbf{C}$ be the category freely generated by objects $x$ and $y$ and morphisms $f: x \to y$ and $g: y \to x$ subject to ….

And if I had to justify the meaning of such definitions (e.g. prove that such a category actually existed), I wouldn’t know what to do except reach for some 2-monad theory.

Of course, in the case of categories, it would be easier to do everything by hand than in the case of PROPs. But as I understand it, being able to do it by hand isn’t the issue — you simply want a reference.

Posted by: Tom Leinster on July 12, 2014 11:35 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Maybe I’m not really understanding the problem here. Based on what you wrote, it seems you’ve got a symmetric monoidal category, and a proof that it’s symmetric monoidally equivalent to the free symmetric monoidal category on objects $x$ and $y$ and morphisms $L$ and $R$, modulo an equation. Given this, I would say it’s perfectly reasonable for you to say that your category ‘has a presentation’. I wouldn’t see much need for you to cite anything in particular except for some category theory textbooks that explain what a symmetric monoidal category is.

Posted by: Jamie Vicary on July 12, 2014 10:00 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

I wonder why it seems to be so hard for mathematicians (myself apparently included) to understand and respond to a pure reference-request question. I’ve asked a few of them myself lately, and they always seem to provoke the kind of response you got from us — “here’s how you could do that very easily”, as if you’d asked “how can I do this?” — rather than an answer to the actual question “who can I cite that has already done this?”

Posted by: Mike Shulman on July 13, 2014 1:08 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Perhaps the thing to do is arXiv a one-page paper on the subject and cite that?

Posted by: Jesse C. McKeown on July 13, 2014 3:40 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

For me it’s hard to give that kind of answer because in fact I don’t know the literature all that well, and it’s usually easier for me to figure it out rather than look it up or head down to a library.

Posted by: Todd Trimble on July 13, 2014 12:38 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

After a couple of years have passed: do we have a standard reference for PROPs generated by (finite) sets of generators and relations, now?

Posted by: Tobias Heindel on February 28, 2017 2:28 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Yes, such a paper exists. It’s not yet finished, but you can see a draft here, and the draft contains most of the material you seem to want:

See Section 4 and Appendix A. I want to generalize all this material to ‘typed’ or ‘colored’ props, which should be quite easy. I hope to finish the paper this spring, since I have no teaching after April. I also have two other papers I need to finish.

Posted by: John Baez on February 28, 2017 6:04 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Interestingly, having completely forgotten this discussion, last summer I spent a bit of time working out a type theory for presenting (colored) props and hence also symmetric monoidal categories. The idea is basically a formalization and generalization of Sweedler notation. As usual, the categorical semantics would show that the well-typed term judgments form the prop presented by whatever generators and relations are used as input for the type theory.

I mostly worked this out while I was writing up notes for the categorical logic course that Peter Lumsdaine and I taught at the AARMS summer school in Dalhousie. But after that was over, I got caught up with other stuff and haven’t done anything more with it yet.

Posted by: Mike Shulman on March 1, 2017 1:26 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Sounds interesting! I’m using a wide variety of props in my work on networks—you can see a bunch of examples in the paper above, and there are a lot more coming. So, any tools that make working with them easier will be appreciated… though the basic questions in my post here are answered to my satisfaction by now.

Posted by: John Baez on March 1, 2017 5:06 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

My motivation was to have an internal language for symmetric monoidal categories, but props are a natural intermediate step. Ordinary type-theoretic judgments like $x:A,y:B,z:C \vdash f(x,y,z):D$ are naturally regarded as presenting a morphism $(A,B,C) \to D$ in a multicategory, where (perhaps cartesian) monoidal categories are regarded as representable multicategories. Similarly, this type theory for props and symmetric monoidal categories has judgments with multiple types on both sides of $\vdash$. (There are other type theories like that, but as far as I know none of them designed for props or symmetric monoidal categories; more common seem to be polycategories or linearly distributive categories.)

The general idea is that a morphism $f:(A,B) \to (C,D)$ in a prop is represented by a list of terms associated to its codomain types containing variables labeling its domain types, such as

$x:A, y:B \vdash (f_{(1)}(x,y), f_{(2)}(x,y)) : (C,D)$

We compose such morphisms by plugging them in for variables, just like in ordinary type theory. For instance, if we also have $g:(C,E) \to H$, then its composite with $f$ is

$x:A, y:B, z:E \vdash (g(f_{(1)}(x,y),z), f_{(2)}(x,y)) : (H,D)$

Here $g$ should really be $g_{(1)}$, but we can omit the subscript when there is only one type in the codomain. To deal with morphisms having no types in the codomain, we have to add an extra list of “scalar terms”; so if we also compose with a morphism $h:(D) \to ()$, then the above term becomes

$x:A, y:B, z:E \vdash (g(f_{(1)}(x,y),z) \mid h(f_{(2)}(x,y))) : (H)$

Finally, if a particular morphism appears more than once in a term-list, we have to distinguish its occurrences with primes. For instance, if $k:() \to (A,B)$, then there are two different composites/tensors of $k$ with itself giving a morphism $() \to (A,A,B,B)$, represented by the two judgments

$\vdash (k_{(1)}, k'_{(1)}, k_{(2)}, k'_{(2)}) : (A,A,B,B)$ $\vdash (k_{(1)}, k'_{(1)}, k'_{(2)}, k_{(2)}) : (A,A,B,B)$

As an example application of this language, a dual of an object $A$ is an object $A^\ast$ with morphisms $\vdash (\eta_{(1)}, \eta_{(2)}) : (A,A^\ast)$ and $x:A^\ast, y:A \vdash (\,\mid\epsilon(x,y)) : ()$ satisfying the triangle identities:

$x:A \vdash (\eta_{(1)} \mid \epsilon(\eta_{(2)},x)) = x : A$ $y:A^\ast \vdash (\eta_{(2)} \mid \epsilon(y,\eta_{(1)}) = y : A^\ast$

If we also have an endomorphism $x:A \vdash f(x):A$ of such an object, then its trace is the “pure scalar”

$\vdash \epsilon(\eta_{(2)}, f(\eta_{(1)})) : ()$

and here is a one-line proof of the cyclicity of trace, $tr(g f) = tr(f g)$, using both triangle identities:

$tr(g f) = (\,\mid \epsilon(\eta_{(2)},g(f(\eta_{(1)})))) = (\,\mid \epsilon(\eta_{(2)},g(\eta'_{(1)})),\epsilon'(\eta'_{(2)},f(\eta_{(1)}))) = (\,\mid \epsilon(\eta'_{(2)},f(g(\eta'_{(1)})))) = tr(f g)$

Posted by: Mike Shulman on March 2, 2017 12:51 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Mike, that’s a really nice syntax. I just wanted to point out another view of PROPs, which leads to a different syntax, and then to ask a question about generalizing yours.

Recall the category of species, which are functors $[\mathbf{Bij}, \mathbf{Set}]$ where $\mathbf{Bij}$ is a category of natural numbers and bijections. Key fact: A prop is the same thing as a commutative monad on $[\mathbf{Bij},\mathbf{Set}]$ that preserves all colimits.

In a paper about quantum computation I came up with a syntax for sifted-colimit-preserving strong monads on $[\mathbf{Bij},\mathbf{Set}]$. So we can use a subset of my syntax to reason about props. This is not surprising because purely quantum computation forms a prop.

In my notation your $f:(A,B)\to(C,D)$ is thought of as having the type $\neg(A,B,\neg(C,D))$, so we can write for instance

(1)$k:\neg (C, D)|a:A,b:B \vdash f(a , b, c.d.k(c,d))$

where the $.$ is variable binding and the $k$ stands for ‘continuation’. Your composite of g and f is notated

(2)$k:\neg (H, D)|a:A,b:B,e:E \vdash f(a , b, c.d. g(c, e, h.k(h,d))$

This syntax completely describes the sifted-colimit-preserving strong monads on species. The downside is that commutativity is not built in. Not all computational monads are commutative, but quantum computation is. (In case this sounds a bit weird: I mean commutative in the sense of commutative versus strong monads; I know that the corresponding *-algebras are non-commutative.)

It would be great if your syntax could be extended to sifted-colimit-preserving commutative monads on species. The only syntax I know is 3-dimensional.

Posted by: Sam Staton on March 3, 2017 10:11 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Thanks! Your syntax with “continuations” reminds me of another sort of syntax that I’ve seen somewhere for type theories whose judgments have multiple consequents as well as multiple antecedents, in which the antecedents are assigned variables and the consequents are assigned “covariables”, and then in between them there is some kind of “term” that describes how the two kinds of variables are matched up. I can’t recall offhand where I saw this though; maybe it was for linearly distributive categories?

I don’t really have any intuition for how a sifted-colimit-preserving monad on species should be regarded as a generalization of a prop. Can you supply any? In particular, can you give an example of how your notation diverges from mine, e.g. some judgment that yours can express but mine can’t, or however the difference manifests itself; it’s not even clear to me what that is. That might help me in speculating about generalizations of my syntax.

(One possible generalization that I have thought a bit about, but it sounds like you’re not as interested in, is to remove commutativity to be talking about “pros” rather than “props”. This turns out to be rather difficult, since the “scalars” have to maintain their location in between the non-scalar terms rather than all being collected at the end of the term, but there are still some commutativities that should be allowed as long as there are no “variable-crossovers”. Peter Lumsdaine and I talked a bit about this last summer, but I don’t recall whether we decided that there was a sensible way to do it.)

Posted by: Mike Shulman on March 3, 2017 11:29 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

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$:

(1)$k:\neg (),l:\neg ()|-\vdash \mathit{new}(a.\mathit{H}(a,a'.\mathit{measure}(a',k(),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,

(2)$k:\neg(C,D)|a:A,b:B\vdash f(a,c.g(b,d.k(c,d)))$
(3)$k:\neg(C,D)|a:A,b:B\vdash g(b,d.f(a,c.k(c,d)))$

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.

Posted by: Sam Staton on March 3, 2017 5:46 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Ah, our comments crossed. I need to think about commutativity and continuations further, but I have one quick question: can your $\neg$’s be arbitrarily nested, e.g. does $\neg (A,B,\neg(C,\neg(D)))$ make sense? Or do they only go two levels deep?

Posted by: Mike Shulman on March 3, 2017 6:46 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Hi, To get a monad, you’re right, you must only go two levels deep. (For syntax, it doesn’t matter what the nesting depth is, and this kind of syntax is quite common in ‘logical frameworks’.)

Moreover, I’ve put two zones in the context: the left zone is non-linear, the right zone is linear. In the profunctor style of your post, a judgement

(1)$k:\neg (A,B),l:\neg (C,D)|e:E,f:F \vdash t$

describes an element of $P(A\otimes B + C\otimes D,E\otimes F)$ where $P:\mathrm{Coprod}(\mathrm{Bij})\looparrowright \mathrm{Bij}$. As you said, substitution is slightly subtle, this is more than just a multicategory, but syntactically it turns out to be the usual substitution for logical frameworks.

Perhaps your idea of two-level bunches will work, I’d like to find time to think about it…

Posted by: Sam Staton on March 4, 2017 11:08 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Okay, I’m starting to get an inkling. A cocontinuous functor between presheaf categories is the same as a profunctor, since a presheaf category is a free cocompletion. Thus, a cocontinuous monad on $[Bij,Set]$ is the same as a monad on $Bij$ in the bicategory $Prof$. A monad in $Prof$ on a category $A$ is the same as a category $B$ with a bijective-on-objects functor $A\to B$. Thus, a cocontinuous monad on $[Bij,Set]$ is the same as a category $B$ with a bijective-on-objects functor $Bij^{op} \to B$. I guess that commutativity of the monad must somehow correspond to a symmetric monoidal structure on this functor, making $B$ a prop.

Analogously, we can regard $[Bij,Set]$ as the free sifted-colimit completion of the free finite-coproduct-completion of $Bij$, call it $Coprod(Bij)$. Thus, a sifted-colimit-preserving endofunctor of $[Bij,Set]$ is the same as a profunctor from $Coprod(Bij)$ to $Bij$, or dually a profunctor from $Bij^{op}$ to $Coprod(Bij)^{op}$. But $Coprod(Bij)^{op} = Prod(Bij^{op})$, the free finite-product completion of $Bij^{op}$, and $Bij^{op}\cong Bij$, so this is the same as a profunctor from $Bij$ to $Prod(Bij)$.

Now, profunctors from $A$ to $Prod(A)$ are also the underlying data of a cartesian multicategory, whose internal language is ordinary “nonlinear intuitionistic simple type theory”. This suggests to me that the judgments for a sifted-colimit-preserving (commutative) monad would have “two-level bunches” in their antecedents, like

$(A,B,C);();(D,E) \vdash (F,G,H)$

where the comma is a “linear” structural connective and the semicolon is a “cartesian” one (admitting contraction and weakening). Semantically, there ought to be a description as a sort of generalized polycategory mixing prop-ness with cartesian-ness. However, I’m not sure what exactly the composition/substitution rule would be, and hence what the terms would look like.

Posted by: Mike Shulman on March 3, 2017 6:42 PM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

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$.

Posted by: Mike Shulman on March 5, 2017 11:53 AM | Permalink | Reply to this

Re: Describing PROPs Using Generators and Relations

Thanks Mike. It occurs to me that perhaps I was trying to run before I can walk: I don’t even know a syntax for commutative algebraic theories without imposing some extra equations. Of course there’s the usual syntax for algebraic theories, plus commutativity axioms. Or there’s Moggi’s monadic metalanguage, where commutativity is just reordering the lines of a program, but you need explicit beta-eta laws for product types or something similar (plus associativity of let etc.). Or I suppose there’s your syntax for props, plus explicit contraction / weakening.

Posted by: Sam Staton on March 10, 2017 7:36 AM | Permalink | Reply to this

Post a New Comment