Non-triviality of *-autonomous categories

Non-triviality of *-autonomous categories

[Harley D. Eades III]

Hi, everyone.  

I am having trouble finding a reference.  I thought perhaps someone here
might know.

It is well known that adding the isomorphism:
   d : A -> (A => 1) => 1
to a bicartisan closed category degenerates to a preorder.

In *-autonomous categories we have such an isomorphism, but
is non-trivial.  Where can I find a proof of this?  I would like to
reference it.  

I think one could proof this using the category of coherence spaces and linear maps
as a concrete *-autonomous category. See for example:

[1] R. a. g. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Computer Science Logic, 1989.

Any references anyone might have would be great.  

Thanks,
.\ Harley




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

Re: Non-triviality of *-autonomous categories

[Michael Barr]

In the original definition, the fact that A --> A** is an isomorphism was
part of the definition.  If that is not what you're asking, then I don't
understand the question.  Of course you have to prove that for Chu
categories, but that was relatively easy.

On Sat, 3 Aug 2013, Harley D. Eades III wrote:

> Hi, everyone.
>
> I am having trouble finding a reference.  I thought perhaps someone here
> might know.
>
> It is well known that adding the isomorphism:
>   d : A -> (A => 1) => 1
> to a bicartisan closed category degenerates to a preorder.
>
> In *-autonomous categories we have such an isomorphism, but
> is non-trivial.  Where can I find a proof of this?  I would like to
> reference it.
>
> I think one could proof this using the category of coherence spaces and linear maps
> as a concrete *-autonomous category. See for example:
>
> [1] R. a. g. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Computer Science Logic, 1989.
>
> Any references anyone might have would be great.
>
> Thanks,
> .\ Harley
>
>

The modern conservative is engaged in one of man's oldest exercises in
moral philosophy--the search for a superior moral justification
for selfishness.  --J.K. Galbraith


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

Re: Non-triviality of *-autonomous categories

[Robert Seely]

If you want *-autonomous categories which are not preorders (I assume
that's what you mean by "non-trivial"), there is an enormous selection
to chose from, including the "first" you mention.  One that's simple
to use is "the" free *-aut cat (over an arbitrary category, so there
are many such free *-aut cats), what we call "circuits" (aka proof
nets). One ref:

   Natural Deduction and Coherence for Weakly Distributive Categories
   (Blute-Cockett-Seely-Trimble) (JPAA 113(1996)3, pp 229-296)

In fact, you can find many examples where the double negation
isomorphism is in fact an equality, by the following result:

   Coherence of the Double Involution on *-Autonomous Categories
   (Cockett-Hasegawa-Seely) (TAC 17(2006) pp 17-29)

(Of course the second paper is online; the first is also available on
my webpage.)

This illustrates Girard's point (made in his first paper on linear
logic) that the double negation isn't inherently non-constructive,
rather that the "problem" with classical logic lies with the contraction
structure rule.

-= rags =-

On Sat, 3 Aug 2013, Harley D. Eades III wrote:

> Hi, everyone.
>
> I am having trouble finding a reference.  I thought perhaps someone here
> might know.
>
> It is well known that adding the isomorphism:
>   d : A -> (A => 1) => 1
> to a bicartisan closed category degenerates to a preorder.
>
> In *-autonomous categories we have such an isomorphism, but
> is non-trivial.  Where can I find a proof of this?  I would like to
> reference it.
>
> I think one could proof this using the category of coherence spaces and linear maps
> as a concrete *-autonomous category. See for example:
>
> [1] R. a. g. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Computer Science Logic, 1989.
>
> Any references anyone might have would be great.
>
> Thanks,
> .\ Harley
>
>
>
-- 
<rags@math.mcgill.ca>
<www.math.mcgill.ca/rags>


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

Re: Non-triviality of *-autonomous categories

[Harley D. Eades III]

Hi, Robert.

On Aug 4, 2013, at 9:10 AM, Robert Seely <rags@math.mcgill.ca> wrote:

> If you want *-autonomous categories which are not preorders (I assume
> that's what you mean by "non-trivial"),
Yes, this is what I meant.  I guess I should have not said "non-trivial", due to
it being somewhat ambiguous. 

> there is an enormous selection
> to chose from, including the "first" you mention.  One that's simple
> to use is "the" free *-aut cat (over an arbitrary category, so there
> are many such free *-aut cats), what we call "circuits" (aka proof
> nets). One ref:
> 
> Natural Deduction and Coherence for Weakly Distributive Categories
> (Blute-Cockett-Seely-Trimble) (JPAA 113(1996)3, pp 229-296)

I have not read this.  Grabbing it now.

> In fact, you can find many examples where the double negation
> isomorphism is in fact an equality, by the following result:
> 
> Coherence of the Double Involution on *-Autonomous Categories
> (Cockett-Hasegawa-Seely) (TAC 17(2006) pp 17-29)
> 
> (Of course the second paper is online; the first is also available on
> my webpage.)
Wonderful!  I will grab this too.

> This illustrates Girard's point (made in his first paper on linear
> logic) that the double negation isn't inherently non-constructive,
> rather that the "problem" with classical logic lies with the contraction
> structure rule.
Indeed, and this point is wonderful, because it tells us that in linear logic
every connective can have a dual without the equational reasoning 
collapsing.  What do I mean by this?  Consider bi-intuitionistic logic.
It is well-known (Crolard:2001) that taking a bi-cartisan closed category
and adding co-exponentials we obtain a preorder.  

What I am working on is showing that we can do a similar construction
using linear categories without degenerating to a preorder in general.
That is taking a linear category and its dual a collinear category and 
smashing them together into what I call a dual linear category. 

Bellin:2012 showed that a collinear category does (unsurprisingly) 
model a co-linear type theory using Crolard's term assignment to
co-inutitionisitc logic.  However, I am a bit dubious of his chosen path.
It is well known that Crolard's subtractive logic is not complete for
bi-intuitionstic logic.  So melding together Bellin's model for 
co-intutionsitic logic, co-linear categories, with linear categories
may not yield a model for bi-intutitionistic linear logic.  So this
seems to be an open question.

Anyway, just thought I would mention what I am working on if
anyone has any feedback.  Thanks for such a quick response.

.\Harley


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