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/ ]