* Non-triviality of *-autonomous categories @ 2013-08-04 0:06 Harley D. Eades III 2013-08-04 13:54 ` Michael Barr ` (2 more replies) 0 siblings, 3 replies; 4+ messages in thread From: Harley D. Eades III @ 2013-08-04 0:06 UTC (permalink / raw) To: categories 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Non-triviality of *-autonomous categories 2013-08-04 0:06 Non-triviality of *-autonomous categories Harley D. Eades III @ 2013-08-04 13:54 ` Michael Barr 2013-08-04 14:10 ` Robert Seely [not found] ` <alpine.LRH.2.03.1308041000010.22374@math.mcgill.ca> 2 siblings, 0 replies; 4+ messages in thread From: Michael Barr @ 2013-08-04 13:54 UTC (permalink / raw) To: Harley D. Eades III; +Cc: categories 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Non-triviality of *-autonomous categories 2013-08-04 0:06 Non-triviality of *-autonomous categories Harley D. Eades III 2013-08-04 13:54 ` Michael Barr @ 2013-08-04 14:10 ` Robert Seely [not found] ` <alpine.LRH.2.03.1308041000010.22374@math.mcgill.ca> 2 siblings, 0 replies; 4+ messages in thread From: Robert Seely @ 2013-08-04 14:10 UTC (permalink / raw) To: Harley D. Eades III; +Cc: categories 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
[parent not found: <alpine.LRH.2.03.1308041000010.22374@math.mcgill.ca>]
* Re: Non-triviality of *-autonomous categories [not found] ` <alpine.LRH.2.03.1308041000010.22374@math.mcgill.ca> @ 2013-08-04 17:44 ` Harley D. Eades III 0 siblings, 0 replies; 4+ messages in thread From: Harley D. Eades III @ 2013-08-04 17:44 UTC (permalink / raw) To: Robert Seely; +Cc: categories 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/ ] ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2013-08-04 17:44 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2013-08-04 0:06 Non-triviality of *-autonomous categories Harley D. Eades III 2013-08-04 13:54 ` Michael Barr 2013-08-04 14:10 ` Robert Seely [not found] ` <alpine.LRH.2.03.1308041000010.22374@math.mcgill.ca> 2013-08-04 17:44 ` Harley D. Eades III
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).