The n-Category Café

Daniel wrote:

If I am very patient, may I be able to write Windows XP using manifolds and cobordisms?

If string theory is correct, Windows XP already runs using manifolds and cobordisms. If loop quantum gravity is correct, it’s using something a bit different, but very similar: spin networks and spin foams.

If Microsoft’s Project Q succeeds, and you’re very patient, you may someday use a version of Windows XP that runs using a modular tensor category implemented via the fractional quantum Hall effect. Read the conclusions of our paper!

But, you may have switched to Vista by then.

How would I halt a program?

I have to admit that this is one part I’m not entirely clear on. There seem to be two approaches to halting, and I’d appreciate the help of the computer science people here in understanding.

The first is the normal form of a term under rewrite rules, which is entirely syntactic. A term has a normal form if the rules are confluent and terminating. This is the case for all terms in the simply-typed lambda calculus, but not in the untyped lambda calculus, since we can write

which rewrites to itself.

The second is interpreting the lambda calculus using (PointedSet, $\wedge$), the symmetric monoidal closed category of pointed sets, pointed maps, and the smash product. The special point of each pointed set is ‘bottom’ ($\bot$), which is used to represent the non-halting state. Pointed maps with the smash product means that if part of the computation takes forever, the whole computation takes forever.

But this means the smash product isn’t cartesian! If you interpret a cartesian closed category $C$ in (PointedSet, $\wedge$), then you have to treat the cartesian product in $C$ as merely a tensor product: you can’t talk about real parallel execution any more. The best you can do is simulate it by threading.

Then there’s some weirdness going on with extensionality, because if you’ve got a language like simply-typed lambda calculus, you may not be able to write an infinite loop, but if you interpret it in PointedSet, you still have to worry about its behavior on bottom.

There’s a thread here where Robin talks about how two programs have the same behavior on all inputs that you can define syntactically, but differ when you feed them ‘parallel or’ (por). Por is not a pointed map with the smash product, but it’s apparently a map in a Scott domain, something I’m not very familiar with. It looks like Scott domains use the cartesian product on pointed sets.

If you use the cartesian product and pick the special point to be $(\bot, \bot),$ then a pointed map out of $X \times Y$ contains more information than a pair of pointed maps, one out of $X$ and one out of $Y$. This is because whereas a pointed map out of $X$ has to send $\bot$ to $\bot,$ a pointed map out of $X \times Y$ can send $(\bot, y)$ (where $y$ is not $\bot$) to something else. (PointedSet, $\times$) is a symmetric monoidal category in which por is a morphism. But (PointedSet, $\times$) is not a closed category, so we can’t interpret lambda calculus there without throwing away closedness. Is a Scott domain closed? How?

We put extensionality into our equivalence rules for the combinator calculus. Is it necessary in order to get a symmetric monoidal closed category?

In a purely functional context like combinator calculus, what are the reduction strategies available to us? How does extensionality play into each of these?

Something about what I just wrote made me even more excited than usual about how ‘cartesianness’ lets us duplicate and delete:

$$x \to x \otimes x$$ $$x \to 1$$

while ‘compactness’ lets us create and annihilate particle-antiparticle pairs:

$$x^* \otimes x \to 1$$ $$1 \to x \otimes x^*$$

This made me ask Jim if he knew of any compact cartesian categories — that is, compact symmetric monoidal categories where the tensor product is the cartesian product and the unit object is terminal.

We soon saw the only example is the terminal category (fun little exercise).

Then Jim said this reminded him of Hawking radiation! Quantum theory lets you create and annihilate particle-antiparticle pairs. A black hole lets you ‘delete’ particles or antiparticles by throwing them down the black hole. The simple idea behind Hawking radiation is that this lets you create particles: create a particle-antiparticle pair, and then delete the antiparticle!

Here we are not using duplication, just deletion. So, I asked Jim a trickier question: are there any compact symmetric monoidal categories where the unit object is terminal?

I’ll leave this as a puzzle. If the only examples are trivial in some sense, it suggests there’s something funny about the simple story of Hawking radiation told above!

Allan wrote:

could we get page numbers?

Yes! You’ve got ‘em now! I apologize to everyone for not including them sooner; I didn’t want to mess with the publisher’s format until the paper had reached a reasonably stable state.

could we imagine adding inference to the Rosetta stone?

I can imagine it… but does it really work? I’d say it ‘works’ if we can describe closed symmetric monoidal categories where ‘beliefs’ are objects and ‘updates’ are morphisms — or something like that. I don’t see precisely how it should go. Has anyone tried something like this?

As for a closed symmetric monoidal category of ‘propositions’ and ‘inferences’, that’s sort of what the logic section is all about. But, sadly, I don’t really understand how Bayesian inference connects to proof theory. Maybe this has something to do with David’s ‘progic’ project?

Last week I had lunch with Carl Hewitt and discussed with him the relationship between the actor model and physics. Hewitt had in mind creation and annihilation operators when conceiving of message passing: one actor “emits” a message, while another “aborbs” the message, and these particles can move around each other. Upon receipt or emission of a message, an actor’s ‘behavior’ changes, but is still considered to be the same actor.

We can get a monoidal category from this by having an object X be “an actor with behavior X” and morphisms be either sending a message

or receiving a message

So roughly, a lambda calculus term is a description of one possible ordering of messages being sent and received. Denotational semantics talks about all possible orderings.

Feynman diagrams were invented to keep track of this kind of thing: each diagram keeps track of one way two systems can interact. The rules of the game tell you how to get all possible interactions.

In physics, more complicated interactions are less probable. This is somewhat related to algorithmic information theory, in that the number of interactions gives a notion of the length of the program, and the probability of each drops off exponentially with the number of interactions or instructions.

Now, since this is the n-Category Café, we really have higher categories in mind. Typed lambda calculus gives a 2-category with objects from types, morphisms from terms, and 2-morphisms from rewrite rules. These rewrite rules happen to be confluent for lambda calculus, so it doesn’t matter in which order you apply them.

The actor model gives a 2-category with objects from types, morphisms from behaviors, and 2-morphisms from sending/receiving a message. These 2-morphisms are not confluent, so you can model two actors vying for the same resource.

Note that in the comparison above, I had to use 1-categories, and the way I got 1-categories from each of these 2-categories was different. With lambda calculus, we can get rid of the 2-morphisms by taking equivalence classes; this is possible because the rewrite rules are confluent.

With the actor model, they’re not confluent, so I had to get rid of the lowest level, the types, instead. I did it by declaring all data types to be isomorphic: every data type is just bits.

As to ditopology, I do not know what the current `best model’ for concurrency is from that direction.

In a paper on the Dagstuhl seminar/conference site, I did look at using simplicially enriched categories and then using bar/cobar type constructions to get a DG category rather as is used in work by Lazaroiu. (My paper is at
kathrin.dagstuhl.de/files/Materials/06/06341/06341.PorterTimothy.Paper!!.pdf)
There may be other papers on that site with relevance to Christine’s question.
The relevant details for that meeting were:

date 20.08.-25.08.06, Seminar Nº 06341

Computational Structures for Modelling Space, Time and Causality

organised by R. Kopperman (City University of New York, US), P. Panangaden (McGill University - Montreal, CA), M. B. Smyth (Imperial College London, GB), D. Spreen (Univ. Siegen, DE)

There are mostly just the abstracts there but there are also links to the proceedings (DROPS submission) for some of the participants.

SVect is also a good example where the re-write rule should not be “(((braid f) x) y) = ((f y) x)”, even though the braiding is symmetric.

Theo’s got a point. The general idea is that if one wants to argue “elementwise” in category theory, one should be prepared to use, instead of (what are sometimes called) “global elements” $I \to X$, “generalized elements” (general morphisms with codomain $X$). For example, in topos theory, it is well known that restriction to global elements is much too crude – there may not be any (for instance, in the topos of sheaves on the unit circle, the universal covering space conceived as an etale space or sheaf has no global elements whatsoever, because that would amount to a global section $S^1 \to \mathbb{R}$)!

One can see this principle at work in the Curry-Howard correspondence between proofs and programs: an equivalence class of proofs $A_1, \ldots, A_n \vdash X$ translates to a term $t(a_1, \ldots, a_n)$ of type $X$ with free variables $a_i$ of types $A_i$. You can think of these free variables as connoting indeterminate generalized elements of type $A_i$ (any term or generalized element of type $A_i$ is allowed to be substituted for the variable $a_i$).

A proof of $I \vdash X$ or of $\vdash X$ would translate to a closed term of type $X$ (no free variables). So your procedure amounts to a decision to consider only closed terms.

SVect is also a good example where the re-write rule should not be “(((braid f) x) y) = ((f y) x)”, even though the braiding is symmetric.

Theo’s right here too. Probably best just to chuck that rewrite rule; just do what you did before in section 3 (mod out by the hexagon etc.).

I can’t call it “Forget”, because it is not fully faithful

It’s a very minor point, but I don’t agree with Theo here. Uncontroversially, you can at least dispense with “full” here; for example the forgetful functor from groups to sets isn’t full.

If one takes the attitude that “forgetful” can only apply to an functor $D \to C$ where objects of $D$ are $C$-objects which come equipped with extra structure and the functor is the one which forgets that structure, then yeah, according to that, faithfulness would be necessary (and Theo is observing here that the functor which remembers only the even-graded part is not faithful – quite right). But we’re in a situation where I’d say that $SuperVect \to Set$ forgets “stuff” as well (namely the odd-graded part). And that language seems perfectly okay to me.

While we’re on the subject of your paper – I’m uneasy with the business of the decision procedure [or coherence problem] for smc categories in section 3. Citing Szabo as having something to do with solving the decision procedure is bound to lead to misunderstanding, and citing my thesis is fine but has the drawback that it’s unpublished. And Kelly and Mac Lane only gave a partial solution.

Here are some other references where a proposed full solution is published and presumably less controversial than Szabo’s (but I really can’t vouch for them personally – I haven’t checked all the details):

• C.B. Jay, The structure of free closed categories, JPAA 66: 271-285 (1990).
• S. Soloviev, Proof of a conjecture of S. Mac Lane, Annals of Pure and Applied Logic 90: 101-162 (1997).

Theo wrote:

Your “extensionally equivalent” condition loses information, when applied to this category: it says that two functions agree if they agree on all even elements.

Yikes! Thanks for catching this. Believe it or not, Mike and I had been fussing about whether to include ‘extensional equivalence’ as part of the definition of when two terms give the same morphism, but I’d been too rushed to give it careful thought. It felt funny to me because of its focus on ‘points’ $x : I \to X$… but for some idiotic reason I didn’t see that it was actually wrong.

I don’t have Lambek and Scott’s book on me here in Singapore, but I believe they did include extensional equivalence as part of their equivalence relation when constructing a cartesian closed category from a theory phrased in terms of the lambda calculus.

I’ll have to go back and check… it now seems wrong to me. Of course your example isn’t cartesian, but the same problem would seem to arise. Say you take a cartesian closed category, turn it into a lambda-theory, then turn it back into a cartesian closed category this way. Then two morphisms $f , f' : X \to Y$ in the original category would now become identified if $fx = f'x$ for every $x : 1 \to X$. This seems like an interesting thing to do to a cartesian closed category — but a highly destructive process in general.

Your other point, about the rewrite rule for the braiding in a symmetric monoidal category, is also well taken. I’ll try to get these problems in the paper fixed before Bob Coecke publishes the darn thing.

I wrote:

…but in combinatory logic, which is what I’m talking about in this section of the paper, there are no variables! All terms are ‘closed’. Right?

Of course, in this setting we can take a ‘generalized element of type $X$’, that is a morphism $x: A \to X$, and curry it to get a ‘closed term of type $A \multimap X$’, that is a morphism $\tilde{x}: I \to (A \multimap X)$. This must be the way out…

… but still, if we have a rewrite rule like

(((braid f) x) y) = ((f x) y)

this seems to apply only to ‘global elements’ $x: I \to X$, $y : I \to Y$, not generalized elements.

So, in SVect, the braiding for homogeneous elements (those entirely even or entirely odd) is $B(a\otimes b) = (-1)^{|a||b|} b\otimes a$, where $|a|$ is $0$ if $a$ is even-graded part and $1$ if $a$ is in the odd-graded part; for general elements, the Braid is extended by (bi)linearity. This matters because it changes the notions of, e.g., when a function is (anti)symmetric. $B$ is an isomorphism between $V\otimes W$ to $W\otimes V$. The functor SVect$\to$Vect that forgets the grading is monoidal but not symmetric monoidal, because it takes $B$ to an isomorphism that is not the usual braiding in Vect.

But, yes, for (even) morphisms $x: I\to X$ and $y: I\to Y$, we certainly have $B(x\otimes y) = (y\otimes x)$. This is true in any braided monoidal category. Because we can untwist open strings:

  I   I          I         I     I   I
  |   |          |         |     |   |
 x|   |y         |         |     |   |
  \   /          /         /    y|   |x
   \ /        I /         /      |   |
    \     =    \    =    /    =  |   |
   / \        / \       /        |   |
  /   \      /   \     /   I     |   |
  |   |     y|   |x   y|   |x    |   |
  |   |      |   |     |   |     |   |

So, in particular, if you only use such global elements, you’ll never be able to pick up braidings that are not symmetric. I think this is probably bad, and means that the rules are missing something. At the very least, the right way to describe a braided monoidal category is to say that $X\otimes Y \to^{f\otimes g} W\otimes V \to^B V\otimes W$ is the same as $X\otimes Y \to^B Y\otimes X \to^{g\otimes f} V\otimes W$, and also that $X\otimes I \to^B I\otimes X \to^L X$ is just $X\otimes I \to^R X$; if you have both of these, then the untwisting follows. ($L$ and $R$ are the left- and right-identity isomorphisms.)

Something you don’t talk about in this section is the associator. As you know, every weakly monoidal category is equivalent to a strict monoidal one (where the associators are identity maps), and also every weakly monoidal category is equivalent to a skeletal one, but you can’t get both.

For example, we have a category equivalent to FinSet which has one set of each cardinalty; I’ll call this set $[n] = \{0,\dots,n-1\} = {Hom}([1],[n])$. We have a (cartesian!) monoidal structure on this. On objects, $[n]\otimes [m] = [n m]$. On morphisms, if $j: [1]\to[n]$ and $i: [1]\to[m]$, then $j\otimes i = j m+i: [1]\to[n m]$.

Ok, so this might violate what I said before. Damn. Because, see, $j\otimes i \neq i\otimes j$. At all. Even though both are global elements (morphisms with domain $= [1]$. On the other hand, this is strictly associative: $k\otimes(j\otimes i) = k n m+j n+i = (k\otimes j)\otimes i$. I’m trying to remember what the natural example of a skeletal non-strict monoidal category is.

So, anyway, I’m just thinking outloud. I’m very nervous, from this example, about your rewrite rules. I’m also uncomfortable that I feel like I proved something to which I provided a counterexample.

I think, overall, that I do not believe that I can push morphisms past the braiding as I did above? Or, rather, the rule is that Braid is not the identity map. But it is, I guess, the Flip map $B(x\otimes y) = y\otimes x$.

Ben, you seem to have lost the bibliography, or at least the version I downloaded was missing the bibliography.

Hi, Ben,

“The conventional measures of information are not appropriate for all situations, and a more general mathematical concept is needed”. Yes, yes! I’ve been trying to make -exactly- that point since 1990 or so (in student eprints and personal communications, later in Usenet postings), but I consistently failed to get this point across to various highly astute mathematicians. I hope you will enjoy better fortune!

Back in 1990, my ideas in brief were (1) to formalize Shannon’s axiomatic approach, using ideas related to lattice theory to remove mention of probability spaces, (2) to formalize some analogies between the easy/general part of classical Galois theory and classical information theory, exploiting an easy/general approach using group actions. I was inspired in part by a remark by my undergraduate algebraic topology (Marshall Cohen) that Noether had noticed that Poincare’s homology groups generalized Betti numbers from numbers to abelian groups, and in part by the Galois duality as per Gelfand between closed subsets in a compact Hausdorff space X and closed ideals of the ring of continuous functions on X. (As everyone here probably knows, here and in classical Galois theory, we have an order reversing duality which “plays nice” which reverses inclusion in the lattice of subgroups/fixsets.) Reading the undergraduate textbook by Davey and Priestly, Introduction to Lattices and Order, was also very helpful to me, particularly the stuff on closure operators and Wille’s “theory of concepts” (which generalizes the remark about lattice structure, and which I tried to popularize for many years). So was an expository paper by Richard Millman, “Kleinian Transformation Geometry”, A. M. Monthly 84 (1977). My interest in both group theory and information theory first arose from a class taught by Martin Harwit (author of an intriguing book, Cosmic Discovery, which IMO was underappreciated when in came out in 1981), who was inspired at least in part by the work of his friend Neil Sloane— who was inspired by his own friend, Claude Shannon!

In an unrelated development, due to some technical problem, yesterday I was unable to post over at Ars Mathematica some background for the award yesterday to Jacques Tits of one half of the 2008 Abel Prize, which I see as evidence of a renewal of interest in the legacy of Klein. Idea (2) falls under this heading, since I used homogeneous spaces (the space of right cosets of a pointwise stabilizers as per Galois) and pointed out that the dimensions of these spaces obey Shannon’s axioms from his 1948 founding paper. (As you know, the axioms you use are significantly different.) It is perhaps notable that over at Not Even Wrong, a few days ago someone suggested Gelfand as possible winner of the Prize; apparently no-one there expected Tits, so obviously there remain conciousnesses to be raised.

Way back in 1994 people were discussing in a once interesting newsgroup, bionet.info-theory, the problem of developing a theory of “biocomplexity”. I had been struck by a chance remark by George C. Williams, Adaptation and Natural Selection (a book often cited as one foundation for the rise of ideas like “kinship selection” in modern evolutionary biology) suggesting that Williams was aware as early as 1966 that “theories of biocomplexity” which assume that organisms are -defined- by their DNA are likely to be based upon a false premise. As I used to put it: naked DNA doth not a bacterium make; you also need complicated “structural overhead”: cell membranes, ribosomes, and so on. Then prevelant ideas concerning the origin of life held that this overhead in fact predated reproduction as we know it. Consequently, I suggested, biologists might need to study notions of “information” or “complexity” which are fundamentally distinct from Shannon’s probalistic formulation.

In particular, I tried hard to make the point that the generality of Shannon’s approach (probability measures can be introduced almost anywhere, after all!) can obscure the fact that using his theory could be completely inappropriate for attempts to capture intuitive ideas of complexity. I pointed out for example that Shannon’s entropies (and my student generalizations) are -subadditive-, whereas biologists might seek measures of “biocomplexity” which are -superadditive-. Unfortunately, I never could seem to get anyone there to understand what I was saying about lattices, closure operators, and so on. (See Davey and Priestly.)

Your list of citations is brief, so I don’t know whether you are aware that there are literally thousands of proposed “information measures” and “complexity measures” in the literature, with almost entirely unknown interrelationships, some of which probably provide examples of your axiomatic approach. In particular, the mathematical ecology literature contains a huge literature on “complexity measures”, some (such as Simpson’s measure) predating Shannon. (Most of the ecologically motivated speculations are profoundly inelegant; some of the mathematically motivated ones are profoundly interesting.) Back around 1994 I wrote two student papers attempting to survey “entropies”, and garnered thousands of references, and venture to guess that the literature has doubled since then.

I may have more substantial comments once I’ve had a chance to study your eprint more closely.

Last but not least, I too wish to thank John and Mike for their excellent paper! I have tried and failed on several occasions to explain some beautiful connections between idea (2) and the lovely reformulation of elementary enumerative combinatorics by Joyal; for some hints see the undergraduate textbook by Cameron, Permutation Groups, and note the close connection between the Joyal cycle index of a structor (combinatorial species) and the Polya index of a finite group action, and thus with the ideas in http://arxiv.org/abs/math/0004133. And the generalization of the “Quotient law” (see Cover and Thomas, Elements of Information Theory) involves Schreier cocycles (see Baumslag and Chandler, Group Theory).

This stuff looks great! I’ve been thinking about this, too–I did my master’s thesis on algorithmic information theory (AIT) and physics, so I’ve been trying to make it mesh with what I’ve been learning.

A prefix-free code is another name for an instantaneous code; you can tell that the message is over once you read the last bit. A prefix-free Turing machine can be considered as a pair of communicating systems: the listening end will wait forever until it gets enough bits for a code word and then will stop reading, while the sending end will wait forever until all the bits it sends have been read. So unless the sender sends exactly one code word, the message (program) is invalid and the computer goes into an infinite loop.

If you use the Lebesgue measure on binary strings (the measure of an n-bit string is $2^{-n}$) then the sum of the measures of valid programs is $\le 1.$ Since the halting programs are a subset of the valid programs, the sum of their measure

This is what Chaitin called the “halting probability” of the prefix-free machine $M$, and proved that for every $M$ there exists $c_M$ such that the shortest program for $M$ outputting the first $n$ bits of $\Omega_M$ is at least $n-c_M$ bits long.

Tadaki generalized $\Omega$ to a zeta function (though he didn’t know it–he was looking at the fractal dimension of the string). He tossed in a scaling factor:

For every $M$ there exists $c_M$ such that for all computable $s$, the shortest program for $M$ outputting the first $n$ bits of $\Omega_M(s)$ is at least $n/s-c_M$ bits long.

In my thesis, I pointed out that it was a stat. mech. zeta function, that the length of the program was like the energy of a state, and looked at a version that was based on natural numbers instead of binary strings. Tadaki followed up with this paper that looks at things like the temperature, energy, entropy, and specific heat in AIT.

I said that the length was like the energy of a state in statistical mechanics. Now I think it actually has more to do with the action of a path, and I should be using a Wick-rotated zeta function: instead of summing the measures $2^{-s |p|}$, sum the actions $exp(i s |p|)$. Since actions add when you compose morphisms, you can often just count the generators in the morphism to get its “measure”, like the interactions in a Feynman diagram or the pants/upside-down pants in a 2Cob morphism.

Michel Lapidus at UCR is researching complex dimensions of fractal strings, defined as the zeros of the zeta function of the fractal string. There ought to be some relation between the complex dimensions he’s looking at and this stuff; I showed in my thesis that there’s information about which programs halt stored in the complex zeros of the zeta function of a Turing machine. He and I looked at analytically continuing the zeta function of a Turing machine to the region $s \le 1,$ but I left before we got anywhere with it. It would be really interesting to know what the information content of $\Omega(s)$ is for $s$ away from the half-line $s\ge 1.$

It turns out that this way of looking at things also works very nicely with the actor model, a model of computation meant to address concurrent systems (and also happens to have excellent security properties, which is why I’m working with them at Google). ‘Actors’ are generating objects in a symmetric monoidal category, and splitting and combining actors (called “sending/receiving a message”) are morphisms. An ‘actor system’ is an arbitrary tensor product of actors. 2Cob is a very simple actor system where circles are actors, pants is sending a message and upside-down pants is receiving a message.

Any specific morphism out of an actor system is one way in which messages could be exchanged. In the actor model, you typically don’t know in advance in what order the messages will be received, so to write a program, you don’t just talk about a single morphism. Instead, you have to think about all possible evolutions, the set of all morphisms out of an object. There’s an embedding of the terms and rewrite rules of untyped lambda calculus into the objects and morphisms of the actor model such that there’s only one morphism out of any given actor system. But in general you can have many morphisms, and this can be used to do concurrent computations—at the expense of dealing with things like race conditions and deadlock.

Are you talking about internal homs or external homs? Since you mention your desire to make hom-tensor duality look pretty, I’ll assume you mean internal hom. For this, our paper uses a notation that’s standard in linear logic:

$$A \multimap B$$

created using ‘\multimap’ in TeX. It’s nice because it looks sort of like a right-pointing arrow, but different enough so you can’t possibly confuse it with all the other right-pointing arrows so important in category theory.

I think this counts as pretty:

$$hom(A \otimes B, C) \cong hom(A , B \multimap C)$$

In our ‘logic’ section we use $A \vdash B$ to mean the external hom: the set of morphisms from $A$ to $B$. This is not standard practice, as far as I can tell — we just did it to emphasize a certain point we were trying to make.

But I don’t know how to generate one in latex

I use this:

\newcommand\lolli{\multimap}
\newcommand\illol{\mathbin{\mathpalette\reflectwithstyle\multimap}}
\newcommand\reflectwithstyle[2]{\reflectbox{\mathsurround=0pt$#1#2$}}

which defines \lolli to be the right-pointing lollipop, and \illol to be the left-pointing one.

You need to include the graphicx package to get \reflectbox. (In case anyone is wondering, the \mathpalette palaver is needed so that it works in subscripts and so forth.)

Of course, a cheap way out would be to say that every braided monoidal closed category gives a braided monoidal combinator calculus satisfying a bunch of rewrite rules, but not claim anything about the converse.

Just a quick comment before I try to say anything more substantial about this business – you’re absolutely right that the rewrite rule for the braiding as applied to global points is correct; this follows from the coherence theorem for braided monoidal categories. I guess I may have been thinking ahead to generalized points, where Theo’s example shows the need for caution, so far as I can tell. Sorry for that confusion.

Thierry wrote:

It seems to me that the reason one needs dinatural transformations is the fact that the variable X in the identity rule (and Y in the cut rule) have both positive and negative occurences.

You’re right. Our ‘explanation’ of the need for dinatural transformations was sloppy. Luckily it’s not too late for us to fix it. Thanks!

Because dinatural transformations do not compose, you cannot get a 2-category out of them. In my opinion, it breaks the beautiful $n$-categorical framework you are showing us. Could you comment on this?

This is a problem Paul–André Melliès and I spent a lot of time on this summer.

It appears that unlike ‘monoidal category’ or ‘symmetric monoidal category’, structures such as ‘monoidal closed category’ or ‘cartesian closed category’ cannot be defined as algebras of a 2-theory in Cat, because variables appear both covariantly and contravariantly — or as you put it, both ‘positively’ and ‘negatively’ — in certain laws.

(See Yanofsky for a convenient introduction to 2-theories: they’re a categorified version of Lawvere’s algebraic theories.)

So, there’s an interesting question: what more general notion ‘theory’ should we use to handle structured categories like these?

When we make some more progress, I’ll report on it here at the Café.

In the same vein, I have the feeling that dual objects in categories are just adjoint in 2-categories with one object. Am I right?

Yes: dual objects in monoidal categories are the same as adjoint morphisms in 2-categories with one object. This is well-known. I spoke about it back in week83, in the Tale of $n$-Categories. But alas, this particular review article is avoiding explicit talk of $n$-categories — except in one section, where I warn the reader that everything here is just the tip of the iceberg. I wanted to minimize the prerequisites.