Re: The boringness of the dual of exponential

[Robert Seely <rags@math.mcgill.ca>]

On Thu, 10 Nov 2011, Vaughan Pratt wrote:

> ...  Well, Set x Set^op is equivalent (in fact
> isomorphic) to Chu(Set, 1).  For *any* set K, both exponentiation and
> dual exponentiation are admissible in Chu(Set,K), product being of the
> tensor kind in this case.
>
> How did I know *that*?  Well, every Chu category is a *-autonomous
> category in the sense of Barr 1979.  If you don't know why every
> *-autonomous category contains both exponentiation and dual
> exponentiation, then like Ebert and Siskel I'm not going to give away
> the plot and you'll just have to fork out to see the movie, or steal it
> if you're a nerd, or watch this space (someone is bound to be a spoiler).

I hadn't intended to say this, but since Vaughan brought up
*-autonomous cats, here goes.  In Cockett-Seely "Proof theory for full
intuitionistic linear logic, bilinear logic, and MIX categories" (TAC
1997) we showed that bilinear logic, formulated with both exponentials
(ie suitable left adjoints to tensoring with an object) and dual
exponentials (ie suitable right adjoints to co-tensoring ("par'ing")
with an object), are just *-autonomous categories.  So not only do
*-autonomous cats have these two types of "internal homs" (4 operators
in all, in the non-symmetric case), but if (eg) a linearly
distributive category has them all, then it must be *-autonomous.  (In
the paper the result is a bit "finer", since we consider two variants
of bilinear logic, the Lambek-style one as above, and what we call
"Grishin categories", BILL and GILL in the paper.  Both amount to
different presentations of *-autonomous cats.)

So, in the non-Cartesian context, suitable duals to exponentials are
anything but boring ...

-= rags =-


-- 
<rags@math.mcgill.ca>
<www.math.mcgill.ca/rags>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]